Abstract
This paper discusses the problem of how to transform a first-order formula into clausal normal form, and to simultaneously construct a proof that the clausal normal form is correct. This is relevant for applications of automated theorem proving where people want to be able to use theorem prover without having to trust it.
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.
Similar content being viewed by others
References
Matthias Baaz, Uwe Egly, and Alexander Leitsch. Normal form transformations. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 5, pages 275–333. Elsevier Science B. V., 2001.
Matthias Baaz and Alexander Leitsch. On skolemization and proof complexity. Fundamenta Informatika, 4(20):353–379, 1994.
Henk Barendregt and Herman Geuvers. Proof-assistents using dependent type systems. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 18, pages 1151–1238. Elsevier Science B.V., 2001.
Stefan Berghofer and Tobias Nipkow. Proof terms for simply typed higher order logic. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher-Order Logics, TPHOLS 2000, volume 1869 of LNCS, pages 38–52. Springer Verlag, 2000.
Marc Bezem, Dimitri Hendriks, and Hans de Nivelle. Automated proof construction in type theory using resolution. In David McAllester, editor, Automated Deduction-CADE-17, number 1831 in LNAI, pages 148–163. Springer Verlag, 2000.
Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software (TACS), volume 1281 of LNCS, pages 515–529, 1997.
Horatiu Cirstea and Claude Kirchner. The rewriting calculus, part 1 + 2. Journal of the Interest Group in Pure and Applied Logics, 9(3):339–410, 2001.
Hans de Nivelle. A resolution decision procedure for the guarded fragment. In Claude Kirchner and Héléne Kirchner, editors, Automated Deduction-CADE-15, volume 1421 of LNCS, pages 191–204. Springer, 1998.
Xiaorong Huang. Translating machine-generated resolution proofs into ND-proofs at the assertion level. In Norman Y. Foo and Randy Goebel, editors, Topics in Artificial Intelligence, 4th Pacific Rim International Conference on Artificial Intelligence, volume 1114 of LNCS, pages 399–410. Springer Verlag, 1996.
William McCune and Olga Shumsky. Ivy: A preprocessor and proof checker for first-order logic. In Matt Kaufmann, Pete Manolios, and J. Moore, editors, Using the ACL2 Theorem Prover: A tutorial Introduction and Case Studies. Kluwer Academic Publishers, 2002? preprint: ANL/MCS-P775-0899, Argonne National Labaratory, Argonne.
Andreas Nonnengart. Strong skolemization. Technical Report MPI-I-96-2-010, Max Planck Institut für Informatik Saarbrücken, 1996.
Andreas Nonnengart and Christoph Weidenbach. Computing small clause normal forms. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 6, pages 335–367. Elsevier Science B. V., 2001.
Hans Jürgen Ohlbach and Christoph Weidenbach. A note on assumptions about skolem functions. Journal of Automated Reasoning, 15:267–275, 1995.
Frank Pfenning. Analytic and non-analytic proofs. In Robert E. Shostak, editor, 7th International Conference on Automated Deduction CADE 7, volume 170 of LNCS, pages 394–413. Springer Verlag, 1984.
Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 17, pages 1065–1148. Elsevier Science B.V., 2001.
R. Sekar, I.V. Ramakrishnan, and Andrei Voronkov. Term indexing. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 26, pages 1853–1964. Elsevier Science B. V., 2001.
Christoph Weidenbach. The spass homepage. http://spass.mpi-sb.mpg.de/.
Christoph Weidenbach. Combining superposition, sorts and splitting. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 27, pages 1965–2013. Elsevier Science B.V., 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Nivelle, H. (2002). Extraction of Proofs from the Clausal Normal Form Transformation. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_39
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive