Structured proof procedures

DOI10.1007/BF01535839zbMath0857.68093OpenAlexW2089317265MaRDI QIDQ1924823

Enrico Giunchiglia, Paolo Pecchiari, Alessandro Armando

Publication date: 3 March 1997

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

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

zbMATH Keywords

interactive theorem prover

Mathematics Subject Classification ID

Uses Software

• GETFOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• Seventy-five problems for testing automatic theorem provers
• Embedding complex decision procedures inside an interactive theorem prover.
• Automated deduction by theory resolution
• Dissolution
• A Proof Method for Quantification Theory: Its Justification and Realization
• An improved proof procedure1
• Nonclausal deduction in first-order temporal logic
• Simplification by Cooperating Decision Procedures
• Theorem Proving via General Matings
• Resolution Strategies as Decision Procedures
• A Computational Study of Satisfiability Algorithms for Propositional Logic
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving