Automated Theorem Proving by Translation to Description Logic

Mapping Intimacies ◽

10.29007/xgq9 ◽

2018 ◽

Author(s):

Negin Arhami ◽

Geoff Sutcliffe

Keyword(s):

Theorem Proving ◽

Propositional Logic ◽

Automated Theorem Proving ◽

Description Logic ◽

Reasonable Time ◽

Intermediate Logics

Many Automated Theorem Proving (ATP) systems for different logics,and translators for translating different logics from one to another,have been developed and are now available.Some logics are more expressive than others, and it is easier to express problems in those logics.However, their ATP systems are relatively newer,and need more development and testing in order to solve more problems in a reasonable time.To benefit from the available tools to solve more problems in more expressive logics,different ATP systems and translators can be combined.Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics.Description Logic (DL) sits between CNF and propositional logic.Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL.ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL,by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.

Download Full-text

PROVA AUTOMATIZADA DE TEOREMA EM LÓGICA PROPOSICIONAL

e-xacta ◽

10.18674/exacta.v6i1.964 ◽

2013 ◽

Vol 6 (1) ◽

pp. 83

Author(s):

Frederico Martins Biber Sampaio ◽

Moisés Henrique Ramos Pereira

Keyword(s):

Theorem Proving ◽

Propositional Logic ◽

Automated Theorem Proving ◽

Proof Methods ◽

Operational Issues ◽

Theoretical Foundations

Este trabalho aborda o desenvolvimento de um sistema para prova automatizada de teoremas em lógica proposicional. O artigo apresenta os fundamentos teóricos gerais, questões operacionais e a estrutura de um software de prova de teoremas, elaborado com propósitos acadêmicos e didáticos, utilizando métodos de prova baseados em três tipos de tableaux semânticos: tableau de Smullyan, tableau com Lema e tableau KE. Experimentos foram realizados para verificar a correção dos resultados das provas, utilizando fórmulas geradas automaticamente.AbstractThis work describes the development of an automated theorem proving system of propositional logic. The paper presents the theoretical foundations, operational issues and structure of a theorem proving software, developed with academic and didactic purposes, using proof methods based on three semantics tableaux: Smullyan tableau, Lema tableau e KE tableau. Experiments were performed to verify the correctness of the results of the proofs, using automatically generating formulas.

Download Full-text

The 10th IJCAR automated theorem proving system competition – CASC-J10

AI Communications ◽

10.3233/aic-201566 ◽

2021 ◽

pp. 1-15

Author(s):

Geoff Sutcliffe

Keyword(s):

Theorem Proving ◽

Classical Logic ◽

Automated Theorem Proving ◽

Fully Automatic

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J10 was the twenty-fifth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition divisions. This paper presents an outline of the competition design, and a commentated summary of the results.

Download Full-text

Retrieval System and Dynamic Algorithm Looking for Axioms of Notions Defined by Programs

Fundamenta Informaticae ◽

10.3233/fi-1993-193-404 ◽

1993 ◽

Vol 19 (3-4) ◽

pp. 275-301

Author(s):

Andrzej Biela

Keyword(s):

Theorem Proving ◽

Dynamic Process ◽

Functional Equations ◽

Automated Theorem Proving ◽

Retrieval System ◽

Formal System ◽

Dynamic Algorithm ◽

Algorithmic Logic ◽

Correctness Of Programs

In this paper we shall introduce a formal system of algorithmic logic which enables us to formulate some problems connected with a retrieval system which provides a comprehensive tool in automated theorem proving of theorems consisting of programs, procedures and functions. The procedures and functions may occur in considered theorems while the program of the above mentioned system is being executed. We can get an answer whether some relations defined by programs hold and we can prove functional equations in a dynamic way by looking for a special set of axioms /assumptions/ during the execution of system. We formulate RS-algorithm which enables us to construct the set of axioms for proving some properties of functions and relations defined by programs. By RS-algorithm we get the dynamic process of proving functional equations and we can answer the question whether some relations defined by programs hold. It enables us to solve some problems concerning the correctness of programs. This system can be used for giving an expert appraisement. We shall provide the major structures and a sketch of an implementation of the above formal system.

Download Full-text