Resolution and model building in the infinite-valued calculus of Łukasiewicz (Q1276262): Difference between revisions
From MaRDI portal
Created a new Item |
Removed claims |
||
Property / author | |||
Property / author: Daniele Mundici / rank | |||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Revision as of 20:23, 10 February 2024
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