Integrating Symbolic Mathematical Computation and Artificial Intelligence

Interactive theorem proving and computer algebra.- A practical algorithm for geometric theorem proving.- Combining theorem proving and symbolic mathematical computing.- Tools for solving problems in the scope of algebraic programming.- Planning a proof of the intermediate value theorem.- A general technique for automatically optimizing programs through the use of proof plans.- Datalog and TwoGroups and C++.- Linear logic and real closed fields: A way to handle situations dynamically.- A proof environment for arithmetic with the omega rule.- Using commutativity properties for controlling coercions.- Theories = signatures + propositions used as types.- The ideal structure of Gröbner base computations.- Modeling cooperating agents scenarios by deductive planning methods and logical fiberings.- Propagation of mathematical constraints in subdefinite models.- Combining computer algebra and rule based reasoning.- Algebraic specification of empirical inductive learning methods based on rough sets and matroid theory.- Subsymbolic processing using adaptive algorithms.- An interpretation of the propositional Boolean algebra as a k-algebra. Effective calculus.- Subdefinite computations and symbolic transformations in the uniCalc solver.