Sciweavers

Share
CADE
2008
Springer
9 years 9 days ago
Title, Preface, Table of Contents
Bernhard Beckert, Gerwin Klein
CADE
2008
Springer
9 years 9 days ago
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
We introduce a DPLL calculus that is a decision procedure for the Bernays-Sch
Leonardo Mendonça de Moura, Nikolaj Bj&osla...
CADE
2008
Springer
9 years 9 days ago
Automated Implicit Computational Complexity Analysis (System Description)
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...
Martin Avanzini, Georg Moser, Andreas Schnabl
CADE
2008
Springer
9 years 9 days ago
Canonical Inference for Implicational Systems
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....
Maria Paola Bonacina, Nachum Dershowitz
CADE
2008
Springer
9 years 9 days ago
Canonicity!
Nachum Dershowitz
CADE
2008
Springer
9 years 9 days ago
Aligator: A Mathematica Package for Invariant Generation (System Description)
We describe the new software package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation and polynomial algebra...
Laura Kovács
CADE
2008
Springer
9 years 9 days ago
Focusing in Linear Meta-logic
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...
Vivek Nigam, Dale Miller
CADE
2008
Springer
9 years 9 days ago
LogAnswer - A Deduction-Based Question Answering System (System Description)
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...
Ulrich Furbach, Ingo Glöckner, Hermann Helbig...
CADE
2008
Springer
9 years 10 months ago
Specification Predicates with Explicit Dependency Information
Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive d...
Richard Bubel, Reiner Hähnle, Peter H. Schmit...
CADE
2008
Springer
9 years 10 months ago
Certificate Translation
Gilles Barthe
books