Proof and Model Generation with Disconnection Tableaux

DOI10.1007/3-540-45653-8_10zbMath1275.03081OpenAlexW55835010MaRDI QIDQ2996159

Gernot Stenz, Reinhold Letz

Publication date: 6 May 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-45653-8_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (7)

Semantically-guided goal-sensitive reasoning: model representation ⋮ The model evolution calculus as a first-order DPLL method ⋮ Comparing instance generation methods for automated reasoning ⋮ The disconnection tableau calculus ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Computing finite models by reduction to function-free clause logic ⋮ First order Stålmarck. Universal lemmas through branch merges

Uses Software

• FINDER
• DCTP

This page was built for publication: Proof and Model Generation with Disconnection Tableaux