Integrating Symbolic Mathematical Computation and Artificial Intelligence, Vol. 958 Book

	Interactive Theorem Proving and Computer Algebra	1
	A Practical Algorithm for Geometric Theorem Proving	10
	Combining Theorem Proving and Symbolic Mathematical Computing	18
	Tools for Solving Problems in the Scope of Algebraic Programming	30
	Planning a Proof of the Intermediate Value Theorem	48
	A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans	64
	Datalog and TwoGroups and C++	80
	Linear Logic and Real Closed Fields: a Way to Handle Situations Dynamically	93
	A Proof Environment for Arithmetic with the Omega Rule	115
	Using Commutativity Properties for Controlling Coercions	131
	Theories = Signatures + Propositions Used as Types	144
	The Ideal Structure of Grobner Base Computations	156
	Modeling Cooperating Agents Scenarios by Deductive Planning Methods and Logical Fiberings	167
	Propagation of Mathematical Constraints in Subdefinite Models	191
	Combining Computer Algebra and Rule Based Reasoning	209
	Algebraic Specification of Empirical Inductive Learning Methods based on Rough Sets and Matroid Theory	224
	Subsymbolic Processing using Adaptive Algorithms	244
	An Interpretation of the Propositional Boolean Algebra as a k-algebra. Effective Calculus	255
	Subdefinite Computations and Symbolic Transformations in the UniCalc Solver	264