Deducibility Constraints

10 years 3 months ago
Deducibility Constraints
In their work on tractable deduction systems, D. McAllester and later D. Basin and H. Ganzinger have identified a property of inference systems (the locality property) that ensures the tractability of the Entscheidungsproblem. On the other hand, deducibility constraints are sequences of deduction problems in which some parts (formulas) are unknown. The problem is to decide their satisfiability and to represent the set of all possible solutions. Such constraints have also been used for deciding some security properties of cryptographic protocols. In this paper we show that local inference systems (actually a slight modification of such systems) yield not only a tractable deduction problem, but also decidable deducibility constraints. Our algorithm not only allows to decide the existence of a solution, but also gives a representation of all solutions.
Sergiu Bursuc, Hubert Comon-Lundh, Stéphani
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2009
Authors Sergiu Bursuc, Hubert Comon-Lundh, Stéphanie Delaune
Comments (0)