Autori: Marin Vlada

Editorial: Kluwer Academic Publishers, Kluwer Academic Publishers, ARTIFICIAL INTELLIGENCE REVIEW, Kluwer Academic Publishers, SSN 0269-2821, vol.15 , No 3, p. pp.153-16, 2001.

Rezumat:

The present paper presents algorithms for testing satisfiabily of clausalformulas in the propositional logic and the firs-order logic. The algorithmbased on the enumeration of solutions for testing the satisfiability ofpropositional formula, has already been given by K. Iwama, O. Dubois. Theoriginality in this paper is to combine this algorithm to other procedures,especially with the pure-literal literal and the one-literal rule, and also theone which consists in changing any formulas in formulas bounded. Thealgorithm based on the enumeration of the solution combined to theseprocedures is more efficient. The algorithm based on the concept ofresolutive derivation from Skolem normal form of formula agr in first-order logic, has already been given. The idea in present’s paper is tocombined to this algorithm to process of elimination of tautological clausesand process of elimination of subsumed clauses.

Cuvinte cheie: first-order logic, propositional logic, resolution method, resolutive derivation, satisfiability

URL: http://www.springerlink.com/content/m63k802mh35p45k3/