CADE
2008
Springer
14 years 11 months ago
2008
Springer
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...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Axiom pinpointing has been introduced in description logics (DL) to help the user understand the reasons why consequences hold by computing minimal subsets of the knowledge base th...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. Conjunctive query answering plays a prominent role in applications of description logics (DLs) that involve instance data, but its exact complexity was a long-standing op...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Security protocols are small programs designed to ensure properties such as secrecy of messages or authentication of parties in a hostile environment. In this paper we investigate ...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security prot...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. We introduce the notion of array-based system as a suittraction of infinite state systems such as broadcast protocols or sorting programs. By using a class of quantified-...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory reasoning. The most efficient SMT solvers rely on refutationa...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
We consider proof systems for effectively propositional logic. First, we show that propositional resolution for effectively propositional logic may have exponentially longer refuta...