Resolution and model building in the infinite-valued calculus of Łukasiewicz (Q1276262)
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: Resolution and model building in the infinite-valued calculus of Łukasiewicz |
scientific article; zbMATH DE number 1243222
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Resolution and model building in the infinite-valued calculus of Łukasiewicz |
scientific article; zbMATH DE number 1243222 |
Statements
Resolution and model building in the infinite-valued calculus of Łukasiewicz (English)
0 references
22 March 1999
0 references
The paper presents a resolution procedure for the infinite-valued calculus of Łukasiewicz. Problems of resolution, model building and their complexity are discussed. The notion of \(\Theta\)-satisfiability is introduced. Then the authors prove that the \(\Theta\)-satisfiability problem is NP-complete. In the particular case of a finite set of Horn-clauses the authors provide decision and model building algorithms that are polynomial. The same is proved for a finite set of Krom-clauses.
0 references
decision algorithm
0 references
resolution procedure
0 references
infinite-valued calculus of Łukasiewicz
0 references
model building
0 references
complexity
0 references
0 references
