Sciweavers

CADE
2000
Springer
14 years 3 months ago
Support Ordered Resolution
Bruce Spencer, Joseph Douglas Horton
CADE
2000
Springer
14 years 3 months ago
System Description: ARA - An Automatic Theorem Prover for Relation Algebras
Abstract. aRa is an automatic theorem prover for various kinds of relation algebras. It is based on Gordeev’s Reduction Predicate Calculi for n-variable logic (RPCn) which allow ...
Carsten Sinz
CADE
2000
Springer
14 years 3 months ago
Machine Instruction Syntax and Semantics in Higher Order Logic
Abstract. Proof-carrying code and other applications in computer security require machine-checkable proofs of properties of machine-language programs. These in turn require axioms ...
Neophytos G. Michael, Andrew W. Appel
CADE
2000
Springer
14 years 3 months ago
Reasoning with Individuals for the Description Logic SHIQ
Abstract. While there has been a great deal of work on the development of reasoning algorithms for expressive description logics, in most cases only Tbox reasoning is considered. I...
Ian Horrocks, Ulrike Sattler, Stephan Tobies
CADE
2000
Springer
14 years 3 months ago
An Infrastructure for Intertheory Reasoning
Abstract. The little theories method, in which mathematical reasoning is distributed across a network of theories, is a powerful technique for describing and analyzing complex syst...
William M. Farmer
CADE
2000
Springer
14 years 3 months ago
Reducing Model Checking of the Many to the Few
E. Allen Emerson, Vineet Kahlon
CADE
2000
Springer
14 years 3 months ago
Automated Proof Construction in Type Theory Using Resolution
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. − A clausification procedure in type theory, equipped w...
Marc Bezem, Dimitri Hendriks, Hans de Nivelle
CADE
2000
Springer
14 years 3 months ago
Two Techniques to Improve Finite Model Search
Abstract. This article introduces two techniques to improve the propagation efficiency of CSP based finite model generation methods. One approach consists in statically rewriting ...
Gilles Audemard, Belaid Benhamou, Laurent Henocque
CADE
2000
Springer
14 years 3 months ago
The Nuprl Open Logical Environment
Abstract. The Nuprl system is a framework for reasoning about mathematics and programming. Over the years its design has been substantially improved to meet the demands of large-sc...
Stuart F. Allen, Robert L. Constable, Richard Eato...