Abstract
Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries. We investigate what canonicity means for implicational systems that are axiomatizations of Moore families – or, equivalently, of propositional Horn theories. We build a correspondence between implicational systems and associative-commutative rewrite systems, give deduction mechanisms for both, and show how their respective inferences correspond. Thus, we exhibit completion procedures designed to generate canonical systems that are “optimal” for forward chaining, to compute minimal models, and to generate canonical systems that are rewrite-optimal. Rewrite-optimality is a new notion of “optimality” for implicational systems, one that takes contraction by simplification into account.
A longer version, “Canonical Ground Horn Theories”, is available as RR49/2007, DI, UniVR at http://profs.sci.univr.it/~bonacina/canonicity.html
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM 41(2), 236–276 (1994)
Bertet, K., Monjardet, B.: The multiple facets of the canonical direct implicational basis. Cahiers de la Maison des Sciences Economiques b05052, Université Paris Panthéon-Sorbonne (June 2005), http://ideas.repec.org/p/mse/wpsorb/b05052.html
Bertet, K., Nebut, M.: Efficient algorithms on the Moore family associated to an implicational system. Discrete Mathematics and Theoretical Computer Science 6, 315–338 (2004)
Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic 8(1), 180–208 (2007)
Bonacina, M.P., Hsiang, J.: On rewrite programs: Semantics and relationship with Prolog. Journal of Logic Programming 14(1 & 2), 155–180 (1992)
Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science 146, 199–242 (1995)
Caspard, N., Monjardet, B.: The lattice of Moore families and closure operators on a finite set: A survey. Electronic Notes in Discrete Mathematics 2 (1999)
Darwiche, A.: Searching while keeping a trace: the evolution from satisfiability to knowledge compilation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130. Springer, Heidelberg (2006)
Dershowitz, N.: Computing with rewrite systems. Information and Control 64(2/3), 122–157 (1985)
Dershowitz, N., Huang, G.-S., Harris, M.A.: Enumeration problems related to ground Horn theories, http://arxiv.org/pdf/cs.LO/0610054
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990)
Dershowitz, N., Marcus, L., Tarlecki, A.: Existence, uniqueness, and construction of rewrite systems. SIAM Journal of Computing 17(4), 629–639 (1988)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulæ. Journal of Logic Programming 1(3), 267–284 (1984)
Furbach, U., Obermaier, C.: Knowledge compilation for description logics. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, Springer, Heidelberg (2007)
Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic 16, 14–21 (1951)
McKinsey, J.C.C.: The decision problem for some classes of sentences without quantifiers. Journal of Symbolic Logic 8, 61–76 (1943)
Roussel, O., Mathieu, P.: Exact knowledge compilation in predicate calculus: the partial achievement case. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 161–175. Springer, Heidelberg (1997)
Sloane, N.J.A.: The On-Line Encyclopedia of Integer Sequences (1996-2006), http://www.research.att.com/~njas/sequences
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonacina, M.P., Dershowitz, N. (2008). Canonical Inference for Implicational Systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-71070-7_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71069-1
Online ISBN: 978-3-540-71070-7
eBook Packages: Computer ScienceComputer Science (R0)