CADE
2008
Springer
14 years 1 months ago
2008
Springer
CADE
2008
Springer
14 years 1 months ago
2008
Springer
We introduce a DPLL calculus that is a decision procedure for the Bernays-Sch
CADE
2008
Springer
14 years 1 months ago
2008
Springer
Recent studies have provided many characterisations of the class of polynomial time computable functions through term rewriting techniques. In this paper we describe a (fully autom...
CADE
2008
Springer
14 years 1 months ago
2008
Springer
Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries....
CADE
2008
Springer
14 years 1 months ago
2008
Springer
CADE
2008
Springer
14 years 1 months ago
2008
Springer
We describe the new software package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation and polynomial algebra...
CADE
2008
Springer
14 years 1 months ago
2008
Springer
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a va...
CADE
2008
Springer
14 years 1 months ago
2008
Springer
LogAnswer is an open domain question answering system which employs an automated theorem prover to infer correct replies to natural language questions. For this purpose LogAnswer o...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive d...
CADE
2008
Springer
14 years 11 months ago
2008
Springer