Sciweavers

AISC
2004
Springer
15 years 18 days ago
Polynomial Interpretations with Negative Coefficients
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpretations with negative coefficients, like x - 1 for...
Nao Hirokawa, Aart Middeldorp
AISC
2004
Springer
15 years 2 months ago
Proof Search in Minimal Logic
ion Within Partial Deduction for Linear Logic . . . . . . . . . . . . . . . . . 52 P. K¨ungas A Decision Procedure for Equality Logic with Uninterpreted Functions . . . 66 O. Tver...
Helmut Schwichtenberg
AISC
2004
Springer
15 years 2 months ago
Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques
Nonlinear constraint systems can be solved by combining consistency techniques and search. In this approach, the search space is reduced using local reasoning on constraints. Howev...
Laurent Granvilliers, Mina Ouabiba
AISC
2004
Springer
15 years 18 days ago
Four Approaches to Automated Reasoning with Differential Algebraic Structures
While implementing a proof for the Basic Perturbation Lemma (a central result in Homological Algebra) in the theorem prover Isabelle one faces problems such as the implementation o...
Jesús Aransay, Clemens Ballarin, Julio Rubi...
AISC
2004
Springer
15 years 2 months ago
A Decision Procedure for Equality Logic with Uninterpreted Functions
The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced...
Olga Tveretina
Artificial Intelligence
Top of PageReset Settings