A comparative study of several proof procedures

DOI10.1016/0004-3702(82)90024-8zbMath0505.68041OpenAlexW2078580799MaRDI QIDQ1836483

Wolfgang Bibel

Publication date: 1982

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(82)90024-8

zbMATH Keywords

algorithms for testing the complementarity of a matrix representing a propositional formulapath through a set of clauses

Mathematics Subject Classification ID

Related Items

An SE-tree-based prime implicant generation algorithm ⋮ On connections and higher-order logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tautology testing with a generalized matrix reduction method
• Refutation graphs
• On the complexity of regular resolution and the Davis-Putnam procedure
• An approach to a systematic theorem proving procedure in first-order logic
• Theorem Proving via General Matings
• On Matrices with Connections
• Refutations by Matings
• A Search Technique for Clause Interconnectivity Graphs
• A Proof Procedure Using Connection Graphs
• A Unifying View of Some Linear Herbrand Procedures