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 = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2009-17.pdf},
}