Inhalt

Invited Presentations.- The Algorithmization of Physics: Math Between Science and Engineering.- Finite Algebras and AI: From Matrix Semantics to Stochastic Local Search.- Proof Search in Minimal Logic.- Planning and Patching Proof.- Papers.- A Paraconsistent Higher Order Logic.- Abstraction Within Partial Deduction for Linear Logic.- A Decision Procedure for Equality Logic with Uninterpreted Functions.- Generic Hermitian Quantifier Elimination.- Extending Finite Model Searching with Congruence Closure Computation.- On the Combination of Congruence Closure and Completion.- Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques.- Proving and Constraint Solving in Computational Origami.- An Evolutionary Local Search Method for Incremental Satisfiability.- Solving Equations Involving Sequence Variables and Sequence Functions.- Verified Computer Algebra in Acl2.- Polynomial Interpretations with Negative Coefficients.- New Developments in Symmetry Breaking in Search Using Computational Group Theory.- Recognition of Whitehead-Minimal Elements in Free Groups of Large Ranks.- Four Approaches to Automated Reasoning with Differential Algebraic Structures.- Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy.- An Expert System on Detection, Evaluation and Treatment of Hypertension.- Short Presentations.- Two Revision Methods Based on Constraints: Application to a Flooding Problem.- Abstraction-Driven Verification of Array Programs.- Singularities in Qualitative Reasoning.- From a Computer Algebra Library to a System with an Equational Prover.