Sergiu Bursuc, Stéphanie Delaune, and Hubert Comon-Lundh. Deducibility constraints. In * Proceedings of the 13th Asian Computing Science Conference (ASIAN'09)*, pp. 24–38, Lecture Notes in Computer Science 5913, Springer, Seoul, Korea, December 2009.

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.

@inproceedings{BCLD-asian09, abstract = {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 \textit{Entscheidungsproblem}.\par 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.\par 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.}, address = {Seoul, Korea}, author = {Bursuc, Sergiu and Delaune, St{\'e}phanie and Comon{-}Lundh, Hubert}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, OPTDOI = {10.1007/978-3-642-10622-4_3}, editor = {Datta, Anupam}, month = dec, pages = {24-38}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Deducibility constraints}, volume = {5913}, year = {2009}, acronym = {{ASIAN}'09}, nmonth = {12}, OPTLONGPDF = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/ rr-lsv-2009-17.pdf}, }