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 | Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2005 - Recent Advances in Artifical Intelligence |
| Editors | I. Russell, Z. Markov |
| Pages | 641-646 |
| Number of pages | 6 |
| State | Published - 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 |
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 |
Fingerprint
ASJC Scopus subject areas
- Engineering(all)
Cite this
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 proceeding › Conference contribution
}
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 -