@inproceedings{f8574bffc70a46a09f25c2782e06d07e,

title = "A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness",

abstract = "The analytic technique for proving completeness gives a very operational perspective: build a countermodel to the unproved formula from a failed proof attempt in your calculus. We have to be careful, however, that the proof attempt did not fail because our strategy in finding it was flawed. Overcoming this concern requires designing a prover. We design and formalize in Isabelle/HOL a sequent calculus prover for first-order logic with functions. We formalize soundness and completeness theorems using an existing framework and extract executable code to Haskell. The crucial idea is to move complexity from the prover itself to a stream of instructions that it follows. The result serves as a minimal example of the analytic technique, a naive prover for first-order logic, and a case study in formal verification.",

keywords = "First-Order Logic, Prover, Completeness, Isabelle/HOL",

author = "From, {Asta Halkj{\ae}r} and J{\o}rgen Villadsen",

year = "2023",

doi = "10.1007/978-3-031-43513-3_25",

language = "English",

isbn = "978-3-031-43512-6",

volume = "14278",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = " 468–480",

booktitle = "Proceedings of the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023",

note = "32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX ; Conference date: 18-09-2023 Through 21-09-2023",

}