A new reduction rule for the connection graph proof procedure

DOI10.1007/BF00297248zbMath0662.68103MaRDI QIDQ1114445

Klaus Heje Munch

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

resolutionautomated theorem provingconnection graphsorder-sorted logic

Mathematics Subject Classification ID

Related Items (2)

Reduction rules for resolution-based systems ⋮ A new subsumption method in the connection graph proof procedure

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Schubert's steamroller problem: Formulations and solutions
• Automated deduction by theory resolution
• On Matrices with Connections
• An Evaluation of an Implementation of Qualified Hyperresolution
• A Proof Procedure Using Connection Graphs

This page was built for publication: A new reduction rule for the connection graph proof procedure