Skip to main content
Conference Proceedings

A mechanically verified, sound and complete theorem prover for first order logic

Lecture Notes in Computer Science (2005) 3603 294-309
DOI: 10.1007/11541868_19
34Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present a system of first order logic, together with soundness and completeness proofs wrt. standard first order semantics. Proofs are mechanised in Isabelle/HOL. Our definitions are computable, allowing us to derive an algorithm to test for first order validity. This algorithm may be executed in Isabelle/HOL using the rewrite engine. Alternatively the algorithm has been ported to OCaML. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Ridge, T., & Margetson, J. (2005). A mechanically verified, sound and complete theorem prover for first order logic. In Lecture Notes in Computer Science (Vol. 3603, pp. 294–309). Springer Verlag. https://doi.org/10.1007/11541868_19

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free