Automated theorem proving methods

DOI10.1007/BF01934987zbMath0564.03016MaRDI QIDQ1057850

Rolf Nossum

Publication date: 1985

Published in: BIT (Search for Journal in Brave)

zbMATH Keywords

surveycompactness methodresolutionmatrix reductionconnection graph

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear unification
• A Proof Method for Quantification Theory: Its Justification and Realization
• An improved proof procedure1
• Theorem Proving via General Matings
• On Matrices with Connections
• A Proof Procedure Using Connection Graphs
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A note on the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem

This page was built for publication: Automated theorem proving methods