Abstract. We discuss a pragmatic approach to integrate computer algebra into proof planning. It is based on the idea to separate computation and veri cation and can thereby exploit...
We define a sound and complete logic, called FO , which extends classical first-order predicate logic with intuitionistic implication. As expected, to allow the interpretation of i...
The behaviour of many systems is naturally modelled by a set of ordinary differential equations (ODEs) which are parametric. Since decisions are often based on relations over these...
In this paper we extend the applicability of our combination method for decision procedures for the word problem to theories sharing non-collapse-free constructors. This extension ...
This paper describes a high-level implementation of the concurrent constraint functional logic language Curry. The implementation, directed by the lazy pattern matching strategy of...