The addition of bounded quantification and partial functions to a computational logic and its theorem prover

DOI10.1007/BF00244392zbMath0653.03007OpenAlexW4248504484MaRDI QIDQ1107510

Robert S. Boyer, J. Strother Moore

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244392

zbMATH Keywords

continuityevaluationrecursionpartial functionssemanticscomputational logicautomated theorem proverinterpreterbounded quantifierspure Lispquantifier-free first- order logic

Mathematics Subject Classification ID

Related Items (7)

On proving the termination of algorithms by machine ⋮ Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks ⋮ A verification system for concurrent programs based on the Boyer-Moore prover ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Limited second-order functionality in a first-order setting ⋮ Programmed Strategies for Program Verification ⋮ Termination analysis for partial functions

Uses Software

• NQTHM

This page was built for publication: The addition of bounded quantification and partial functions to a computational logic and its theorem prover