Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse





Synthesizing semantics for extensions of propositional logic


Ohlbach,  Hans Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)

(Any fulltext), 256KB

Supplementary Material (public)
There is no public supplementary material available

Ohlbach, H. J.(1994). Synthesizing semantics for extensions of propositional logic (MPI-I-94-225). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as:
Given a Hilbert style specification of a propositional extension of standard propositional logic, it is shown how the basic model theoretic semantics can be obtained from the axioms by syntactic transformations. The transformations are designed in such a way that they eliminate certain derived theorems from the Hilbert axiomatization by turning them into tautologies. The following transformations are considered. Elimination of the reflexivity and transitivity of a binary consequence relation yields the basic possible worlds framework. Elimination of the congruence properties of the connectives yields weak neighbourhood semantics. Elimination of certain monotonicity properties yields a stronger neighbourhood semantics. Elimination of certain closure properties yields relational possible worlds semantics for the connectives. If propositional logic is the basis of the specification, the translated Hilbert axioms can be simplified by eliminating the formula variables with a quantifier elimination algorithm. This way we obtain the frame conditions for the semantic structures. All transformations work for arbitrary n-place connectives. The steps can be fully automated by means of PL1 theorem provers and quantifier elimination algorithms. The meta theory guarantees soundness and completeness of all transformation steps. As a by--product, translations into multi--modal logic are developed.