TY - JOUR
T1 - Semantic derivation verification
T2 - Techniques and implementation
AU - Sutcliffe, Geoff
N1 - Copyright:
Copyright 2008 Elsevier B.V., All rights reserved.
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 -