Abstract
Many problems can be specified by patterns of propositional formulae depending on a parameter, e.g. the specification of a circuit usually depends on the number of bits of its input. We define a logic whose formulae, called iterated schemata, allow to express such patterns. Schemata extend propositional logic with indexed propositions, e.g.P i, P i + 1, P 1 or P n, and with generalized connectives, e.g. \(\bigwedge_{\rm i = 1}^n\), or \(\bigvee_{\rm i = 1}^n\), where n is an (unbound) integer variable called a parameter. The expressive power of iterated schemata is strictly greater than propositional logic: it is even out of the scope of first-order logic. We define a proof procedure, called dpll ⋆ , that can prove that a schema is satisfiable for at least one value of its parameter, in the spirit of the dpll procedure [9]. But proving that a schema is unsatisfiable for every value of the parameter, is undecidable [1] so dpll ⋆ does not terminate in general. Still, dpll ⋆ terminates for schemata of a syntactic subclass called regularly nested.
This work has been partly funded by the project ASAP of the French Agence Nationale de la Recherche (ANR-09-BLAN-0407-01).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus For Propositional Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 32–46. Springer, Heidelberg (2009)
Aravantinos, V., Caferra, R., Peltier, N.: A Decidable Class of Nested Iterated Schemata (extended version). Technical report, Laboratory of Informatics of Grenoble (2010), http://arxiv.org/abs/1001.4251
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)
Bradfield, J., Stirling, C.: Modal Mu-Calculi. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier Science Inc., New York (2007)
Bundy, A.: The Automation of Proof by Mathematical Induction. In: [13], pp. 845–911
Comon, H.: Inductionless induction. In: [13], ch. 14
Cooper, D.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7. Edinburgh University Press (1972)
Corcoran, J.: Schemata: the concept of schema in the history of logic. The Bulletin of Symbolic Logic 12(2), 219–240 (2006)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communication of the ACM 5, 394–397 (1962)
Fagin, R.: Finite-Model Theory - A Personal Perspective. Theoretical Computer Science 116, 3–31 (1993)
Kapur, D., Subramaniam, M.: Extending Decision Procedures with Induction Schemes. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 324–345. Springer, Heidelberg (2000)
Orevkov, V.P.: Proof schemata in Hilbert-type axiomatic theories. Journal of Mathematical Sciences 55(2), 1610–1620 (1991)
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier, Amsterdam (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aravantinos, V., Caferra, R., Peltier, N. (2010). A Decidable Class of Nested Iterated Schemata. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-14203-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14202-4
Online ISBN: 978-3-642-14203-1
eBook Packages: Computer ScienceComputer Science (R0)