AISC
2004
Springer
13 years 8 months ago
2004
Springer
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...
AISC
2004
Springer
13 years 8 months ago
2004
Springer
We present a new method for generic quantifier elimination that uses an extension of Hermitian quantifier elimination. By means of sample computations we show that this generic Her...
AISC
2004
Springer
13 years 8 months ago
2004
Springer
Abstract. Origami (paper folding) has a long tradition in Japan's culture and education. We are developing a computational origami system, based on symbolic computation system...
AISC
2004
Springer
13 years 8 months ago
2004
Springer
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...
AISC
2004
Springer
13 years 10 months ago
2004
Springer
AISC
2004
Springer
13 years 10 months ago
2004
Springer
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...
AISC
2004
Springer
13 years 10 months ago
2004
Springer
ion Within Partial Deduction for Linear Logic . . . . . . . . . . . . . . . . . 52 P. K¨ungas A Decision Procedure for Equality Logic with Uninterpreted Functions . . . 66 O. Tver...
AISC
2004
Springer
13 years 10 months ago
2004
Springer
AISC
2004
Springer
13 years 10 months ago
2004
Springer
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...
AISC
2004
Springer
13 years 10 months ago
2004
Springer
Qualitative Reasoning is characterised by making knowledge explicit in order to arrive at efficient reasoning techniques. It contrasts with often intractable quantitative models. W...