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 language | English (US) |
|---|---|
| Pages (from-to) | 1053-1070 |
| Number of pages | 18 |
| Journal | International Journal on Artificial Intelligence Tools |
| Volume | 15 |
| Issue number | 6 |
| DOIs | |
| State | Published - Dec 2006 |
Fingerprint
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 journal › Article
}
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 -