Semantic Derivation Verification

Geoff Sutcliffe and Diego Belfiore, University of Miami

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.