Electronic Resource
Springer
Annals of mathematics and artificial intelligence
12 (1994), S. 231-263
ISSN:
1573-7470
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
,
Mathematics
Notes:
Abstract We generalize prepositional semantic tableaux for classical and many-valued logics toconstraint tableaux. We show that this technique is a generalization of the standard translation from CNF formulas into integer programming. The main advantages are (i) a relatively efficient satisfiability checking procedure for classical, finitely-valued and, for the first time, for a wide range of infinitely-valued propositional logics; (ii) easy NP-containment proofs for many-valued logics. The standard translation of two-valued CNF formulas into integer programs and Tseitin's structure preserving clause form translation are obtained as a special case of our approach.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01530787
Permalink
|
Location |
Call Number |
Expected |
Availability |