Sciweavers

TPHOL
2005
IEEE
13 years 9 months ago
A HOL Theory of Euclidean Space
We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is RN with the...
John Harrison
IPPS
2006
IEEE
13 years 9 months ago
An overview of the Jahob analysis system: project goals and current status
We present an overview of the Jahob system for modular analysis of data structure properties. Jahob uses a subset of Java as the implementation language and annotations with formu...
Viktor Kuncak, Martin C. Rinard
CADE
2004
Springer
14 years 3 months ago
Experiments on Supporting Interactive Proof Using Resolution
Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be...
Jia Meng, Lawrence C. Paulson
CADE
2008
Springer
14 years 3 months ago
THF0 - The Core of the TPTP Language for Higher-Order Logic
One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This p...
Christoph Benzmüller, Florian Rabe, Geoff Sut...
CADE
2009
Springer
14 years 4 months ago
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
The Thousands of Problems for Theorem Provers (TPTP) problem library is the basis of a well established infrastructure supporting research, development, and deployment of first-ord...
Chad E. Brown, Christoph Benzmüller, Frank Th...