Quantified Multimodal Logics in Simple Type Theory (bibtex)
by Christoph Benzmüller, Lawrence Paulson
Abstract:
We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.
Reference:
Quantified Multimodal Logics in Simple Type Theory (Christoph Benzmüller, Lawrence Paulson), SEKI Publications (ISSN 1437-4447), SEKI Report SR-2009-02 (ISSN 1437-4447), 2009. (arXiv:0905.2435)
Bibtex Entry:
@techreport{R45,
  Abstract =	 {We present a straightforward embedding of quantified
                  multimodal logic in simple type theory and prove its
                  soundness and completeness. Modal operators are
                  replaced by quantification over a type of possible
                  worlds.  We present simple experiments, using
                  existing higher-order theorem provers, to
                  demonstrate that the embedding allows automated
                  proofs of statements in these logics, as well as
                  meta properties of them.},
  Address =	 {{DFKI Bremen GmbH, Safe and Secure Cognitive
                  Systems, Cartesium, Enrique Schmidt Str.\,5,
                  D--28359 Bremen, Germany}},
  Author =	 {Benzm{\"u}ller, Christoph and Paulson, Lawrence},
  Note =	 {arXiv:0905.2435},
  Institution =	 {Saarland University},
  Publisher =	 {{SEKI Publications (ISSN 1437-4447)}},
  Series =	 {{SEKI Report SR-2009-02 (ISSN 1437-4447)}},
  Title =	 {Quantified Multimodal Logics in Simple Type Theory},
  Url =		 {http://arxiv.org/abs/0905.2435},
  Year =	 2009,
}
Powered by bibtexbrowser