QMLTP-Library ReadMe ********************* The Quantified Modal Logic Theorem Proving (QMLTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for first-order modal logic. It includes a comprehensive set of problems for various first-order modal logics in an extended TPTP-syntax and tools for converting the problems into some of the existing modal theorem prover formats. It also includes information about ATP-systems for first-order modal logic and their perfomance results on the benchmark problems. Please see also http://www.iltp.de/qmltp. Installation ------------ Unpack and untar QMLTP-v1.1.tar.gz > tar -xzf QMLTP-v1.1.tar.gz This will create the directory QMLTP-v1.1 Contents -------- * Problems - benchmark problems in a standardised syntax * Axioms - axioms supplying the embedding of quantified modal logic into simple type theory (STT): needed for the higher-order ATP systems (Leo-II, Satallax) * TPTP2X - tools for converting the problem into some of the existing modal ATP system format * Documents - performance results on the benchark problems for ATP systems in quantified modal logics, statistics, example sessions, ReadMe.qmltp - this file tptp2X ------ This tool that translates problems into the syntax of the respective ATP system. It stems from the TPTP-Library [2] and is adapted to the QMLTP-library: - it includes format-files for some modal ATP systems and for generation of problems by applying geodel's empbedding on classical first-order problems - it is extended by modal operators (box, dia) - adding equality axioms is adapted to modal logic (for adding equality axioms in classical or intuitionistic logic, use > cp transform.equality.orig transform.equality - it is adapted to the directory structure of the QMLTP-Library You will need some Prolog Interpreter. For full details see the technical maunal at http://www.cs.miami.edu/~tptp. a) Configure tptp2X tool: > cd QMLTP-v0.2/TPTP2X > ./tptp2X_install This script will ask for required information: path of the ILTP directory, Prolog dialect (ECLiPSe, SWI, SISCtus, YAP), absolute path name of the executable Prolog Interpreter, the ATP system you want to translate the problems to (simply type 'a' for 'all'). b) Use TPTP2X tool to translate problems: > ./tptp2X -f [-t ] ../Problems//'*.p' This will write the translated problems into the directory . The parameters are: : one of mleantap (for MleanTAP, MleanSeP), gqmlprover (for GQML-Prover), thf (for TPTP THF-format of higher-order logic theorem prover like LEO-II, Satallax) : one of APM, GAL, GLC, GNL, GSE, GSV, GSY, SYM, NLP, SET : add_equality: - adds equality axioms - necessary, if the prover has no special method for handling equality - not stable under SWI-Prolog. do not use shorten, beacause it would generate faulty transformed problems logic: - only if is thf : k, d, t, s4, s5 for the respective modal logic Benchmark Problems ------------------ QMLTP-v1.1: 600 problems: 580 uni-modal (330 non-propositional, 170 propositional) 20 multi-modal (13 non-propositional, 7 propoisitional) sources: applications, textbooks, TANCS-2000, TPTP-v5.0.0, Goedel translation - each problem is associated with useful header information - modal status and rating wrt. particular first-order modal logic and domain condition in v1.1: uni-modal first-order logics K, D, T, S4, S5, varying, cumulative constant domain multi-modal logics with intended logics for each modality operator, cumulative domain term condition: rigid, local terms Theorem : problem was proven by some modal ATP system Non-Theorem: problem was refuted by some modal ATP system Unsolved : status could not be determined by any modal ATP system under the test conditions difficulty rating: 0.0 .. 1.0 ratio of the current modal state-of-the-art ATP systems which fail to prove or refute the problem (0.0: easy, ... 1.0: hard) state-of-the-art ATP system: ATP system whose set of solved problems are not subsumed by another ATP system - description, source, references Test conditions --------------- time limit: 600 sec. Xeon 3.4 GHz, 4 GB RAM, Linux 2.6.24-24.x86_64 Mandrake 10.2 ATP system : GQML-Prover MleanTAP MleanCoP MleanSeP f2p+MSPASS Leo-II Satallax version : 1.2 1.3 1.2 1.2 1.1/3.0 1.2.6 2.2 programming language : OCaml Prolog Prolog Prolog Prolog OCaml Lisp compiler : OCaml 3.10 ECLiPSe v5.10 ECLiPSe v5.10 ECLiPSe v5.10 ECLiPSe v5.10/ gcc v. 4.6.1 Ocaml 3.10 Steel Bank Common Lisp Contact ------- Please contact us, if you have any questions, suggestions, or if you have developed an ATP system or benchmark problems for first-order modal logic. We would like to include your ATP system and your benchmark problems in the QMLTP-library. Thomas Raths: traths@cs.uni-potsdam.de Jens Otten http://www.iltp.de/qmltp Theoretical Computer Science Institute of Computer Science University of Potsdam Postfach 90 03 27 D-14439 Potsdam Germany Tel. +49 331 977-3041 Fax: +49 331 977-3042 References ---------- [1] K. Goedel. An interpretation of the intuitionistic sentential logic. In J. Hintikka, Ed., The Philosophy of Mathematics, S. 128--129. Oxford University Press, 1969. [2] G. Sutcliffe, C. Suttner. The TPTP problem library - CNF release v1.2.1. Journal of Automated Reasoning, 21: 177-203, 1998. http://www.cs.miami.edu/~tptp/