An extension of the Boyer-Moore theorem prover to support first-order quantification
From MaRDI portal
Publication:688572
DOI10.1007/BF00245295zbMath0784.68076MaRDI QIDQ688572
Publication date: 4 January 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Set theory for verification. I: From foundations to functions
Uses Software
Cites Work
