Sciweavers

4 search results - page 1 / 1
» tableaux 1995
Sort
View
CSL
1995
Springer
13 years 8 months ago
Deduction by Combining Semantic Tableaux and Integer Programming
In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an ...
Bernhard Beckert, Reiner Hähnle
TABLEAUX
1995
Springer
13 years 8 months ago
Constraint Model Elimination and a PTTP-Implementation
In constraint logic programming, proof procedures for Horn clauses are enhanced with an interface to efficient constraint solvers. In this paper we show how to incorporate constra...
Peter Baumgartner, Frieder Stolzenburg
TABLEAUX
1995
Springer
13 years 8 months ago
A Connection Based Proof Method for Intuitionistic Logic
We present a proof method for intuitionistic logic based on Wallen’s matrix characterization. Our approach combines the connection calculus and the sequent calculus. The search t...
Jens Otten
TABLEAUX
1995
Springer
13 years 8 months ago
On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs
We present a procedure transforming intuitionistic matrix proofs into proofs within the intuitionistic standard sequent calculus. The transformation is based on L. Wallen’s proof...
Stephan Schmitt, Christoph Kreitz