Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CRYPTO
2011
Springer
222views Cryptology» more  CRYPTO 2011»
9 years 6 months ago
Computer-Aided Security Proofs for the Working Cryptographer
Abstract. We present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches—compact, formal representations of the essence of a...
Gilles Barthe, Benjamin Grégoire, Sylvain H...
CADE
2011
Springer
9 years 6 months ago
Experimenting with Deduction Modulo
Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through rules rewriting terms and proposi...
Guillaume Burel
AICOM
2010
129views more  AICOM 2010»
10 years 6 months ago
Automated theorem proving in quasigroup and loop theory
We survey all known results in the area of quasigroup and loop theory to have been obtained with the assistance of automated theorem provers. We provide both informal and formal d...
J. D. Phillips, David Stanovský
CADE
2010
Springer
10 years 7 months ago
Analytic Tableaux for Higher-Order Logic with Choice
Abstract. While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers currently do not. As a step towards supporting autom...
Julian Backes, Chad E. Brown
IJCAI
1997
10 years 7 months ago
High Performance ATP Systems by Combining Several AI Methods
We present a design for an automated theorem prover that controls its search based on ideas from several areas of artificial intelligence (AI). The combination of case-based reaso...
Jörg Denzinger, Marc Fuchs, Matthias Fuchs
TABLEAUX
2000
Springer
10 years 10 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
FOIKS
2006
Springer
10 years 10 months ago
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover
It is claimed in [45] that first-order theorem provers are not efficient for reasoning with ontologies based on description logics compared to specialised description logic reasone...
Ian Horrocks, Andrei Voronkov
CADE
1992
Springer
10 years 10 months ago
Caching and Lemmaizing in Model Elimination Theorem Provers
Theorem provers based on model elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we repor...
Owen L. Astrachan, Mark E. Stickel
CADE
1994
Springer
10 years 10 months ago
PROTEIN: A PROver with a Theory Extension INterface
Abstract. PROTEIN (PROver with a Theory Extension INterface) is a PTTPbased first order theorem prover over built-in theories. Besides various standardrefinements knownformodelelim...
Peter Baumgartner, Ulrich Furbach
IFM
2005
Springer
100views Formal Methods» more  IFM 2005»
10 years 11 months ago
Embedding the Stable Failures Model of CSP in PVS
We present an embedding of the stable failures model of CSP in the PVS theorem prover. Our work, extending a previous embedding of the traces model of CSP in [6], provides a platfo...
Kun Wei, James Heather
books