Accelerating tableaux proofs using compact representations
type: Item
instance of: scholarly article
title: Accelerating tableaux proofs using compact representations
zbMATH Open document ID: 0808.03006
DOI: 10.1007/BF01384237
author: Klaus Schneider
author: Ramayya Kumar
author: Thomas Kropf
published in: Formal Methods in System Design
publication date: 1994-09-26T00:00:00Z
review text: A modified form of tableau calculus, called tableau graph calculus, is introduced. The aim is to overcome the well-known inefficiencies of the traditional tableau calculus. The new calculus is based on a compact representation of analytic tableaux by using tableau graphs. Such graphs can be generated from the input formula in linear time. As a result, the tableau graph calculus has only a single rule that is repeatedly applied to obtain a proof. Many optimization heuristics are presented as well.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 644675
zbMATH Keywords: tableau calculus
zbMATH Keywords: tableau graph
MaRDI profile type: Publication
cites work: On Extensions of Elementary Logic
cites work: Q3753927
cites work: Q3753930
cites work: Structuring and automating hardware proofs in a higher-order theorem- proving environment
cites work: Untersuchungen über das logische Schliessen. I
cites work: Theorem Proving via General Matings
cites work: Matings in matrices
cites work: Q4182465
cites work: Q3996619
cites work: Proof methods for modal and intuitionistic logics
cites work: Q3997615
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Linear unification
cites work: An Efficient Unification Algorithm
cites work: About the Paterson-Wegman linear unification algorithm
cites work: Q5560258
cites work: First-order modal tableaux
cites work: Seventy-five problems for testing automatic theorem provers
cites work: Q4282596
cites work: A Proof Procedure Using Connection Graphs
Recommended article: A tableaux calculus for reducing proof size
Recommended article: Q2721210
Recommended article: A compact representation of proofs
Recommended article: The proof complexity of analytic and clausal tableaux
Recommended article: Q2754047
Recommended article: Q4858952
Recommended article: Proving as fast as computing: succinct arguments with constant prover overhead
Recommended article: Q4992506
Recommended article: A fast saturation strategy for set-theoretic tableaux
Recommended article: Optimal Tableau Algorithms for Coalgebraic Logics
description: scientific article; zbMATH DE number 644675