A comparative study of several proof procedures

DOI10.1016/0004-3702(82)90024-8zbMATH Open0505.68041OpenAlexW2078580799MaRDI QIDQ1836483FDOQ1836483

Authors: 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

Cites Work

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

Cited In (3)

• Computing prime implicants
• An SE-tree-based prime implicant generation algorithm
• On connections and higher-order logic

This page was built for publication: A comparative study of several proof procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1836483)