Tautology testing with a generalized matrix reduction method

DOI10.1016/0304-3975(79)90054-9zbMath0421.03011OpenAlexW2028359267WikidataQ127775962 ScholiaQ127775962MaRDI QIDQ1132862

Wolfgang Bibel

Publication date: 1979

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(79)90054-9

zbMATH Keywords

Presburger arithmeticgeneralizing Prawitz' matrix reduction for tautology testing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05)

Related Items (4)

On the relative merits of path dissolution and the method of analytic tableaux ⋮ On connections and higher-order logic ⋮ A comparative study of several proof procedures ⋮ The linked conjunct method for automatic deduction and related search techniques

Cites Work

• Non-resolution theorem proving
• Computer proofs of limit theorems
• A Human Oriented Logic for Automatic Theorem-Proving
• Towards feasible solutions of the tautology problem
• Theorem Proving by Covering Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Tautology testing with a generalized matrix reduction method