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 ...
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 ...
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...
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...
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...
Abstract. This article introduces two techniques to improve the propagation efficiency of CSP based finite model generation methods. One approach consists in statically rewriting ...
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...