Semantic derivation verification: Techniques and implementation

Research output: Contribution to journalArticle

24 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 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 languageEnglish (US)
Pages (from-to)1053-1070
Number of pages18
JournalInternational Journal on Artificial Intelligence Tools
Volume15
Issue number6
DOIs
StatePublished - Dec 1 2006

Keywords

  • Automated theorem proving
  • Derivation verification

ASJC Scopus subject areas

  • Artificial Intelligence

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

  • Cite this