In this poster session, we present the current results of on-going projects on deduction, disjunctive logic programming, and information management systems, at the University of Koblenz, Germany. The central idea behind these projects is to apply techniques and concepts developed for theorem proving in disjunctive logic programming (thereby achieving a tight integration between these two paradigms) and apply this combination to real world problems such as information management systems. The theorem prover PROTEIN developed as a result of the deduction project is being extended to include features, such as minimal model reasoning, that are required for disjunctive logic programming. In the sequel, we briefly review this idea. Interested readers are referred to our full papers (see the references) for more information on the presented materials. PROTEIN (PROver with a Theory Extension INterface) is a complete theorem prover for first order clause logic implemented in ECLiPSe-Prolog, based on the Prolog Technology Theorem Proving (PTTP) technique. Salient features of this theorem prover include constraint handling and theory reasoning. It includes theory reasoning in a very general way. An auxiliary program can be used to derive a suitable background reasoner from a given Horn theory in a fully automatic way. Moreover, the framework of constraint model elimination has been developed and so PROTEIN can exploit the constraint solvers usually used in the field of constraint logic programming. Interested readers are referred to [BF94a, BF94b, BFS95, BS95], for more information on PROTEIN and the calculi behind it.
展开▼
