Semantic derivation verification

Geoffrey Sutcliffe, Diego Belfiore

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 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 such unsoundness, the derivations output by an ATP system may be semantically verified by a trusted system that checks the required semantic properties of each inference step. Such verification may need 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 in the DVDV verifier.

Original languageEnglish (US)
Title of host publicationProceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence
EditorsI. Russell, Z. Markov
Pages641-646
Number of pages6
StatePublished - 2005
EventRecent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Clearwater Beach, FL, United States
Duration: May 15 2005May 17 2005

Other

OtherRecent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005
CountryUnited States
CityClearwater Beach, FL
Period5/15/055/17/05

Fingerprint

Theorem proving
Semantics

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Sutcliffe, G., & Belfiore, D. (2005). Semantic derivation verification. In I. Russell, & Z. Markov (Eds.), Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence (pp. 641-646)

Semantic derivation verification. / Sutcliffe, Geoffrey; Belfiore, Diego.

Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence. ed. / I. Russell; Z. Markov. 2005. p. 641-646.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Sutcliffe, G & Belfiore, D 2005, Semantic derivation verification. in I Russell & Z Markov (eds), Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence. pp. 641-646, Recent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005, Clearwater Beach, FL, United States, 5/15/05.
Sutcliffe G, Belfiore D. Semantic derivation verification. In Russell I, Markov Z, editors, Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence. 2005. p. 641-646
Sutcliffe, Geoffrey ; Belfiore, Diego. / Semantic derivation verification. Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence. editor / I. Russell ; Z. Markov. 2005. pp. 641-646
@inproceedings{91a46d232dce4a1086b31fe44725590b,
title = "Semantic derivation verification",
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 such unsoundness, the derivations output by an ATP system may be semantically verified by a trusted system that checks the required semantic properties of each inference step. Such verification may need 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 in the DVDV verifier.",
author = "Geoffrey Sutcliffe and Diego Belfiore",
year = "2005",
language = "English (US)",
isbn = "1577352343",
pages = "641--646",
editor = "I. Russell and Z. Markov",
booktitle = "Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence",

}

TY - GEN

T1 - Semantic derivation verification

AU - Sutcliffe, Geoffrey

AU - Belfiore, Diego

PY - 2005

Y1 - 2005

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 such unsoundness, the derivations output by an ATP system may be semantically verified by a trusted system that checks the required semantic properties of each inference step. Such verification may need 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 in the DVDV 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 such unsoundness, the derivations output by an ATP system may be semantically verified by a trusted system that checks the required semantic properties of each inference step. Such verification may need 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 in the DVDV verifier.

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

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

M3 - Conference contribution

AN - SCOPUS:32844462916

SN - 1577352343

SP - 641

EP - 646

BT - Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence

A2 - Russell, I.

A2 - Markov, Z.

ER -