An extension of the Boyer-Moore theorem prover to support first-order quantification.

*(English)*Zbl 0784.68076Summary: We describe an implementation of an extension to the Boyer-Moore Theorem Prover and logic that allows first-order quantification. The extension retains the capabilities of the Boyer-Moore system while allowing the increased flexibility in specification and proof that is provided by quantifiers. The idea is to Skolemize in an appropriate manner. We demonstrate the power of this approach by describing three successful proof-checking experiments using the system, each of which involves a theorem of set theory as translated into a first-order logic. We also demonstrate the soundness of our approach.

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

03C07 | Basic properties of first-order languages and structures |

##### Software:

NQTHM
PDF
BibTeX
XML
Cite

\textit{M. Kaufmann}, J. Autom. Reasoning 9, No. 3, 355--372 (1992; Zbl 0784.68076)

Full Text:
DOI

##### References:

[1] | BoyerR. S. and MooreJ S., A Computational Logic Handbook, Academic Press, Boston (1988). |

[2] | Goldschlag David M., ?Mechanically verifying concurrent programs with the Boyer-Moore prover?, IEEE Transactions on Software Engineering, SE-16(9) (September 1990). |

[3] | Goldschlag, David M., ?Proving proof rules: A proof system for concurrent programs?, Compass ’90 (June 1990). |

[4] | Goldschlag, David M., ?Mechanizing Unity?, in: Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods, M. Broy and C. B. Jones (Eds.), Elsevier Science Publishers B.V. (1990). |

[5] | Yu Yuan, ?Computer proofs in group theory?, J. Automated Reasoning, 6(3) (September 1990). · Zbl 0702.68094 |

[6] | Kaufmann, Matt, ?A user’s manual for an interactive enhancement to the Boyer-Moore Theorem Prover?, Tech. Report 19, Computational Logic, Inc. (May 1988). |

[7] | Kaufmann, Matt, ?Addition of free variables to an interactive enhancement of the Boyer-Moore Theorem Prover?, Tech. Report 42, Computational Logic, Inc. (May 1989). |

[8] | deChampeauxD., ?Subproblem finder and instance checker, two cooperating modules for theorem provers?, J. Assoc. Comp. Mach. 33, 633-657 (October 1986). |

[9] | Kaufmann, Matt, ?DEFN-SK: An extension of the Boyer-Moore Theorem Prover to handle first-order quantifiers?, Tech. Report 43, Computational Logic, Inc. (May 1989). |

[10] | McCarthy, J., Abrahams, P. W., Edwards, D. J., Hart, T. P., and Levin, M. I., MIT LISP 1.5 Programmer’s Manual, MIT (1962). |

[11] | ShoenfieldJ. R., Mathematical Logic, Addison-Wesley, Reading, Mass. (1967). |

[12] | Boyer, Robert S., Goldschlag, David M., Kaufmann, Matt, and Moore, J Strother, ?Functional instantiation in first order logic?, Tech. Report 44, Computational Logic, Inc. (May 1989). · Zbl 0755.68120 |

[13] | Ketonen, Jussi, ?EKL ? Ramsey theorem?, Tech. Report, Department of Computer Science, Stanford University (December 1986). |

[14] | KunenKenneth, Set Theory: An Introduction to Independence Proofs, North-Holland, New York (1980). |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.