Reasoning Systems as Semantic Reasoning Web Services:
We described several types of reasoning systems as Semantic Web Services:1. Problem Transformation Systems
MathServe currently offers three services for the translation of proving problems in classical first-order predicate logic with equality into clause normal form (CNF): The Flotter service can be used to generate efficient CNFs. It integrates an improved version of renaming, optimized and strong Skolemisation, and efficient redundancy tests [3]. The tptp2X utility can be used to create simple CNFs and also to translate problems into the input languages of many first-order ATP systems. The tool is available with the TPTP Library. The Tramp Clause Normaliser creates CNFs similar to the ones created by tptp2X. However, together with the CNF it also delivers a delta-relation, i.e. a mapping of from the literals in the CNF to formula positions in the original first-order formula. This mapping is crucial for constructing proofs in Natural Deduction (ND) calculus out of refutations for CNFs.
In the future we are also planning to integrate other problem transformation services such as higher-order to first-order translators. Or services that translate essentially propositional logic into problems for SAT solvers.2. Automated Theorem Provers
We integrated the ATP systems Otter, Ep, Spass and Vampire. All ATP services get a problem description in the new TPTP format and a time limit in seconds as an input. The problem is transformed into the provers' input format using the tptp2X utility. The result specifies the status of the given problem with one of the statuses defined in the SZS Status Ontology. If the system delivered a refutation proof then the proof is also translated into TSTP format (optionally in XTSTP) using tools developed by Geoff Sutcliffe.
The OWL-S ATP services are annotated with performance data of the underlying ATP systems on the TPTP Library (V. 3.0.1). The MathServe Broker uses this data to choose a suitable prover for a problem at hand.3. Proof Transformation Tools
MathServe currently offers three proof transformation tools. The Otterfier service can translate arbitrary resolution proofs into proofs using only binary resolution, factoring and paramodulation as inference rules (i.e., Otter's BrFP calculus). Unfortunately, the current version of Otterfier is rather slow.
Given a TSTP conjecture in FOF format and a resolution proof for the CNF of that problem, the Tramp ND Service can translate that resolution proof into a Natural Deduction proof of the original conjecture.
OWL-S Services:
This is our representation of the OWL-S profile of the Tramp ND Service:
The full OWL-S service descriptions for first-order ATP services can be found here. OWL-S descriptions of transformation services are here.
This page is under construction!
Contact:
Last modified: Fri Sep 22 17:00:55 CEST 2006