SEMANTIC DERIVATION VERIFICATION: TECHNIQUES AND IMPLEMENTATION

GEOFF SUTCLIFFE

doi:10.1142/s0218213006003119

SEMANTIC DERIVATION VERIFICATION: TECHNIQUES AND IMPLEMENTATION

International Journal of Artificial Intelligence Tools ◽

10.1142/s0218213006003119 ◽

2006 ◽

Vol 15 (06) ◽

pp. 1053-1070 ◽

Cited By ~ 13

Author(s):

GEOFF SUTCLIFFE

Keyword(s):

Theorem Proving ◽

Automated Theorem Proving ◽

Verification Techniques ◽

Semantic Properties

Automated Theorem Proving (ATP) systems are complex pieces of software, and thus may have bugs that make them unsound. In order to guard against unsoundness, the derivations output by an ATP system may be semantically verified by trusted ATP systems that check the required semantic properties of each inference step. Such verification needs to be augmented by structural verification that checks that inferences have been used correctly in the context of the overall derivation. This paper describes techniques for semantic verification of derivations, and reports on their implementation and testing in the GDV verifier.

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