Semantic derivation verification: Techniques and implementation

Research output: Contribution to journalArticlepeer-review

24 Scopus citations


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
Issue number6
StatePublished - Dec 2006


  • Automated theorem proving
  • Derivation verification

ASJC Scopus subject areas

  • Artificial Intelligence


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

Cite this