Semantic derivation verification: Techniques and implementation

Research output: Contribution to journalArticle

24 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Pages (from-to)1053-1070
Number of pages18
JournalInternational Journal on Artificial Intelligence Tools
Volume15
Issue number6
DOIs
StatePublished - Dec 2006

Fingerprint

Theorem proving
Semantics
Testing

Keywords

  • Automated theorem proving
  • Derivation verification

ASJC Scopus subject areas

  • Artificial Intelligence

Cite this

Semantic derivation verification : Techniques and implementation. / Sutcliffe, Geoffrey.

In: International Journal on Artificial Intelligence Tools, Vol. 15, No. 6, 12.2006, p. 1053-1070.

Research output: Contribution to journalArticle

@article{a5837738a457499cb021cd50c565013d,
title = "Semantic derivation verification: Techniques and implementation",
abstract = "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.",
keywords = "Automated theorem proving, Derivation verification",
author = "Geoffrey Sutcliffe",
year = "2006",
month = "12",
doi = "10.1142/S0218213006003119",
language = "English (US)",
volume = "15",
pages = "1053--1070",
journal = "International Journal on Artificial Intelligence Tools",
issn = "0218-2130",
publisher = "World Scientific Publishing Co. Pte Ltd",
number = "6",

}

TY - JOUR

T1 - Semantic derivation verification

T2 - Techniques and implementation

AU - Sutcliffe, Geoffrey

PY - 2006/12

Y1 - 2006/12

N2 - 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.

AB - 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.

KW - Automated theorem proving

KW - Derivation verification

UR - http://www.scopus.com/inward/record.url?scp=33845667991&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845667991&partnerID=8YFLogxK

U2 - 10.1142/S0218213006003119

DO - 10.1142/S0218213006003119

M3 - Article

AN - SCOPUS:33845667991

VL - 15

SP - 1053

EP - 1070

JO - International Journal on Artificial Intelligence Tools

JF - International Journal on Artificial Intelligence Tools

SN - 0218-2130

IS - 6

ER -