Semantic derivation verification

Geoff Sutcliffe; Diego Belfiore

Semantic derivation verification

Geoff Sutcliffe, Diego Belfiore

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Scopus citations

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 language	English (US)
Title of host publication	Recent Advances in Artifical Intelligence - Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005
Editors	I. Russell, Z. Markov
Pages	641-646
Number of pages	6
State	Published - Dec 1 2005
Event	Recent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Clearwater Beach, FL, United States Duration: May 15 2005 → May 17 2005

Publication series

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

Other

Other	Recent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005
Country	United States
City	Clearwater Beach, FL
Period	5/15/05 → 5/17/05

ASJC Scopus subject areas

Engineering(all)

Fingerprint Dive into the research topics of 'Semantic derivation verification'. Together they form a unique fingerprint.

Cite this

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

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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sutcliffe, G & Belfiore, D 2005, Semantic derivation verification. in I Russell & Z Markov (eds), Recent Advances in Artifical Intelligence - Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005. 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, Recent Advances in Artifical Intelligence - Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005. 2005. p. 641-646. (Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence).

Sutcliffe, Geoff ; Belfiore, Diego. / Semantic derivation verification. Recent Advances in Artifical Intelligence - Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005. editor / I. Russell ; Z. Markov. 2005. pp. 641-646 (Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence).

@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 = "Geoff Sutcliffe and Diego Belfiore",

year = "2005",

month = dec,

day = "1",

language = "English (US)",

isbn = "1577352343",

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

pages = "641--646",

editor = "I. Russell and Z. Markov",

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

note = "Recent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 ; Conference date: 15-05-2005 Through 17-05-2005",

}

TY - GEN

T1 - Semantic derivation verification

AU - Sutcliffe, Geoff

AU - Belfiore, Diego

PY - 2005/12/1

Y1 - 2005/12/1

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

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

SP - 641

EP - 646

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

A2 - Russell, I.

A2 - Markov, Z.

T2 - Recent Advances in Artifical Intelligence - Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005

Y2 - 15 May 2005 through 17 May 2005

ER -