Accelerating tableaux proofs using compact representations (Q1334905)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Accelerating tableaux proofs using compact representations |
scientific article |
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
