Resolution and model building in the infinite-valued calculus of Łukasiewicz
type: Item
instance of: scholarly article
title: Resolution and model building in the infinite-valued calculus of Łukasiewicz
zbMATH Open document ID: 0921.03013
DOI: 10.1016/S0304-3975(98)00012-7
author: N. Olivetti
author: Daniele Mundici
published in: Theoretical Computer Science
publication date: 1999-03-22T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B50
zbMATH DE Number: 1243222
zbMATH Keywords: decision algorithm
zbMATH Keywords: resolution procedure
zbMATH Keywords: infinite-valued calculus of Łukasiewicz
zbMATH Keywords: model building
zbMATH Keywords: complexity
reviewed by: Nail Zamov
MaRDI profile type: Publication
cites work: Exploiting data dependencies in many-valued logics
cites work: The decision problem for formulas in prenex conjunctive normal form with binary disjunctions
cites work: A theorem about infinite-valued sentential logic
cites work: Satisfiability in many-valued sentential logic is NP-complete
cites work: Logic of infinite quantum systems
cites work: Q3837739
cites work: Optimal comparison strategies in Ulam's searching game with two errors
cites work: Fragments of Many-Valued Statement Calculi
description: scientific article; zbMATH DE number 1243222