The application of automated reasoning to questions in mathematics and logic

DOI10.1007/BF01543481zbMath0997.03500WikidataQ114267028 ScholiaQ114267028MaRDI QIDQ1354049

Larry Wos, William W. McCune

Publication date: 13 May 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

automated reasoningOTTERproof findingcombinatory logicfinite semigroupRobbins algebraequivalential calculusconjecture formulationobject construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Uses Software

• OTTER
• AURA
• NQTHM
• SbReve2
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• Meeting the challenge of fifty years of logic
• Using automated reasoning tools: A study of the semigroup \(F_ 2B_ 2\)
• A case study in automated theorem proving: Finding sages in combinatory logic
• Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• The lambda calculus, its syntax and semantics
• Complexity and related enhancements for automated theorem-proving programs
• A shortest single axiom for the classical equivalential calculus
• Proof Checking the RSA Public Key Encryption Algorithm
• Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• New Sets of Independent Postulates for the Algebra of Logic, With Special Reference to Whitehead and Russell's Principia Mathematica
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving