Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Synthesizing semantics for extensions of propositional logic

Ohlbach, Hans J├╝rgen

MPI-I-94-225. June 1994, 45 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Categories / Keywords: Logic, semantics, transformation
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-225.pdfMPI-I-94-225.pdfMPI-I-94-225.dvi224 KBytes; 255 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Ohlbach, Hans J{\"u}rgen},
  TITLE = {Synthesizing semantics for extensions of propositional logic},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-225},
  MONTH = {June},
  YEAR = {1994},
  ISSN = {0946-011X},