Resolution and model building in the infinite-valued calculus of Łukasiewicz (Q1276262)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Resolution and model building in the infinite-valued calculus of Łukasiewicz |
scientific article |
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