Accelerating tableaux proofs using compact representations (Q1334905)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Accelerating tableaux proofs using compact representations |
scientific article; zbMATH DE number 644675
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Accelerating tableaux proofs using compact representations |
scientific article; zbMATH DE number 644675 |
Statements
Accelerating tableaux proofs using compact representations (English)
0 references
26 September 1994
0 references
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.
0 references
tableau calculus
0 references
tableau graph
0 references
0 references
0 references
0 references
0.8677123
0 references
0.85811514
0 references
0.85388285
0 references
0.8516222
0 references
