IMPLEMENTING COMPLEX DOMAINS OF APPLICATION IN AN EXTENDED PROLOG SYSTEM

One way to extend resolution based theorem proving is by means of unification in algebras modelling interesting domains of application. We will discuss in this paper the theoretical and practical aspects of unification in the unitarytheory of Post algebras, which cover among others boolean algebras, algebras formalizing multivalued logic and finite fields. Therefore, a theorem prover using unification in Post algebras is capable of dealing with the design of digital circuits, combinatorics, applications of multivalued logic and mathematics over finite fields.