Sciweavers

CADE
2010
Springer
13 years 6 months ago
Interpolation and Symbol Elimination in Vampire
It has recently been shown that proofs in which some symbols are colored (e.g. local or split proofs and symbol-eliminating proofs) can be used for a number of applications, such a...
Krystof Hoder, Laura Kovács, Andrei Voronko...
TABLEAUX
2000
Springer
13 years 9 months ago
MSPASS: Modal Reasoning by Translation and First-Order Resolution
mspass is an extension of the first-order theorem prover spass, which can be used as a modal logic theorem prover, a theorem prover for description logics and a theorem prover for ...
Ullrich Hustadt, Renate A. Schmidt
CADE
2004
Springer
14 years 6 months ago
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software
Abstract. We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof ...
Bernd Fischer 0002, Ewen Denney, Johann Schumann