Font Size: a A A

# Automated theorem proving by translation to description logic

Posted on:2016-08-09Degree:Ph.DType:Dissertation
University:University of MiamiCandidate:Arhami, NeginFull Text:PDF
GTID:1478390017477617Subject:Computer Science
Abstract/Summary:
Many Automated Theorem Proving (ATP) systems for different logical forms, and translators for translating different logical forms from one to another, have been developed and are now available. Some logical forms are more expressive than others, and it is easier to express problems in those logical forms. On the other hand, the ATP systems for less expressive forms have benefited from more years of development and testing. There is a trade-off between the expressivity of a logical form, and the capabilities of the available ATP systems. Different ATP systems and translators can be combined to solve a problem expressed in a given logical form. In this research, an experiment has been designed and carried out to compare all different possible ways of trying to solve a problem, using the following logical forms in increasing order of expressivity: Propositional Logic, Description Logic, Effectively Propositional form, Conjunctive Normal Form, First Order Form, Typed First order form-monomorphic, Typed First order form-polymorphic, Typed Higher order form-monomorphic. In this dissertation, the properties, syntax, and semantics of each target logical form are briefly described. For each form, the most popular ATP systems and translators for translating to less expressive forms are introduced.;Problems in logics more expressive than Conjunctive Normal Form can be translated directly to Conjunctive Normal Form, or indirectly by translation via intermediate logics. No translator was available to translate from Conjunctive Normal Form to Description Logic, which sits between Effectively Propositional form and Propositional Logic in terms of expressivity. Saffron a Conjunctive Normal Form to Description Logic translator, has been developed, which fills the gap between Conjunctive Normal Form and Description Logic. Moreover, Description Logic Form (DLF), a new syntax for Description Logic, has been designed. Automated theorem proving by translation to Description Logic is now an alternative way of solving problems expressed in logics more expressive than Description Logic, by combining necessary translators from those logics to Conjunctive Normal Form, Saffron, and a Description Logic ATP system.
Keywords/Search Tags:Logic, Automated theorem proving, Form, ATP, Translators, Translation, Different
Related items
 1 The Research On The Extension Rule Based Theorem Proving 2 Research On Some Automated Reasoning Methods For Logic 3 Set Theory Equation Type Theorem Proving Systems Research And Development 4 Based On Ontology And Prolog Rules Of Geometry Theorem Proving 5 Model checking and theorem proving: A unified framework 6 Methods For Overcoming Two Kinds Of Deficiencies Of Automated Theorem Provers In Program Verification 7 SEMANTIC PARAMODULATION FOR HORN SETS (LOGIC, EQUALITY, THEOREM-PROVING) 8 The Constructions Of A Parallel Interactive Theorem Prover 9 Study On A First-order Logic Automated Theorem Prover Based On Contradiction Separation Deduction 10 TPaxos In PaxosStore:Specification,Refinement,and Theorem Proving