Model, Fixpoint, and Herbrand Semantics for Quantified Disjunctive Programs

Dušan Guller

In the talk, we shall present model, fixpoint, and Herbrand semantics for quantified disjunctive programs with equality, sets of formulae in prenex conjunctive normal form. We shall proceed from the declarative semantics concerning only logical consequences of a given program P: DS(P) = {C | C is a formula in prenex conjunctive normal form, P ⊧ C}. The model semantics is proposed by means of clausal models [1, 2]. We introduce a class of clausal models, one of conservative extensions of the class of first-order models. We shall firstly discuss the relation between clausal and first-order models. Secondly, we establish the notion of a characteristic clausal model for a quantified disjunctive program. Such a model satisfies exactly the formulae being logical consequences of the program. We further prove the characterisation theorem: If a quantified disjunctive program P has a clausal model, then P has a characteristic clausal model 𝔐, which is constructible by a closure operator C. This model 𝔐 will be taken as the basis for the model semantics of the program P: MS(P) = {C | C is a formula in prenex conjunctive normal form, 𝔐 ⊧^{∨} C}; and by the least fixpoint of the operator C, we define the fixpoint semantics for P. In conclusion, we shall deal with a generalised statement of Herbrand’s theorem, which applies to quantified disjunctive programs without adding Skolem and Herbrand function symbols [3]. This extended Herbrand’s theorem gives us some characterisation of logical consequences of a quantified disjunctive program in terms of tautological following. By this statement, we establish the Herbrand semantics. As an immediate consequence of the characterisation theorem, we obtain the coincidence of these semantics.

[1] Guller, D. Semantics for disjunctive programs. Proceedings of the Fifth Workshop of Logic, Language, Information and Computation, 79-91, 1998. Abstract in the Logic Journal of the IGPL, Oxford University Press, Vol. 6, N. 6, November 1998.

[2] Guller, D. On clausal models. Proceedings of the Sixth Workshop of Logic, Language, Information and Computation, 1999. Abstract in the Logic Journal of the IGPL, Oxford University Press, Vol. 7, N. 4, July 1999.

[3] Guller, D. One generalisation of Herbrand’s theorem. Proceedings of the Second Panhellenic Logic Symposium, 1999.

Address: Institute of Informatics, Comenius University, Mlynská dolina, 842 15 Bratislava, Slovakia

E-mail: guller@fmph.uniba.sk