Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras

Author

Sofronie-Stokkermans, Viorica

Author_Institution

Max-Planck-Inst. fur Inf., Saarbrucken, Germany

fYear

2004

fDate

19-22 May 2004

Firstpage

32

Lastpage

37

Abstract

In this paper, we present a resolution-based decision procedure which can be used for deciding unification with linear constant restriction for a large class of finitely-generated varieties of algebras. Since the decidability of V-unification with linear constant restrictions implies the decidability of the positive theory of V, the method presented above yields a decision algorithm for the positive theory of V. The method is based on the existence of natural duality theorems for such classes of algebras.

Keywords

algebra; computability; decidability; decision theory; duality (mathematics); V-unification decidability; finitely generated algebra positive theory; linear constant restriction unification; natural duality theorems; representation theorems; resolution-based decision procedures; satisfiability problems; unifiability; Bibliographies; Boolean algebra; Character generation; Encoding; Equations; Knowledge representation; Lattices; Logic; Modules (abstract algebra); System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Multiple-Valued Logic, 2004. Proceedings. 34th International Symposium on

ISSN

0195-623X

Print_ISBN

0-7695-2130-4

Type

conf

DOI

10.1109/ISMVL.2004.1319916

Filename

1319916