Lemma matching for a PTTP-based top-down theorem prover

DOI10.1007/3-540-63104-6_16zbMath1430.68413OpenAlexW1559498617MaRDI QIDQ5234698

Koji Iwanuma

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_16

zbMATH Keywords

automated reasoninginference ruletheorem provermodel eliminationlemma matching rule

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Controlled use of clausal lemmas in connection tableau calculi

Uses Software

• SETHEO
• OTTER
• SATCHMO
• HARP
• METEOR

Cites Work

• Unnamed Item
• Unnamed Item
• Near-Horn prolog and beyond
• What is the inverse method?
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• The use of lemmas in the model elimination procedure
• SATCHMORE: SATCHMO with RElevancy
• The disconnection method
• Hyper tableaux
• A Simplified Format for the Model Elimination Theorem-Proving Procedure