Logic Programming and Automated Reasoning Book

	Soundness and Completeness of Partial Deductions for Well-Founded Semantics	1
	On Deductive Planning and the Frame Problem	13
	On Resolution in Fragments of Classical Linear Logic	30
	A Procedure for Automatic Proof Nets Construction	42
	Free Logic and Infinite Constraint Networks	54
	Towards Probabilistic Knowledge Bases	66
	Two-Level Grammar: A Functional/Logic Query Language for Database and Knowledge-Base Systems	78
	Extending Deductive Database Languages by Embedded Implications	84
	Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years	96
	Resolution for Many-Valued Logics	107
	An Ordered Theory Resolution Calculus	119
	Application of Automated Deduction to the Search for Single Axioms for Exponent Groups	131
	Elementary Lower Bounds for the Lengths of Refutations	137
	Shortening Proofs by Quantifier Introduction	148
	Reform Compilation for Nonlinear Recursion	160
	Pruning Infinite Failure Branches in Programs with Occur-Check	172
	The Use of Planning Critics in Mechanizing Inductive Proofs	178
	[lambda][mu]-Calculus: An Algorithmic Interpretation of Classical Natural Deduction	190
	Building Proofs by Analogy via the Curry-Howard Isomorphism	202
	On the Use of the Constructive Omega-Rule Within Automated Deduction	214
	OR-Parallel Theorem Proving with Random Competition	226
	Parallel Computation of Multiple Sets-of-Support	238
	Towards Using the Andorra Kernel Language for Industrial Real-Time Applications	250
	Unification in a Combination of Equational Theories with Shared Constants and its Application to Primal Algebras	261
	Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria	273
	Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems	285
	A Two Step Semantics for Logic Programs with Negation	297
	Generalized Negation as Failure and Semantics of Normal Disjunctive Logic Programs	309
	General Model Theoretic Semantics for Higher-Order Horn Logic Programming	320
	Disjunctive Deductive Databases	332
	Netlog - A Concept Oriented Logic Programming Language	357
	From the Past to the Future: Executing Temporal Logic Programs	369
	Computing Induction Axioms	381
	Consistency of Equational Enrichments	393
	A Programming Logic for a Verified Structured Assembly Language	403
	The Unification of Infinite Sets of Terms and its Applications	409
	Unification in Order-Sorted Type Theory	421
	Infinite, Canonical String Rewriting Systems Generated by Completion	433
	Spes: A System for Logic Program Transformation	445
	Linear Objects: A Logic Framework for Open System Programming	448
	ISAR: An Interactive System for Algebraic Implementation Proofs	451
	Mathpert: Computer Support for Learning Algebra, Trig and Calculus	454
	MegaLog - A Platform for Developing Knowledge Base Management Systems	457
	SPIKE, an Automatic Theorem Prover	460
	An Application to Teaching in Logic Course of ATP Based on Natural Deduction	463
	A Generic Logic Environment	466
	ElipSys. A Parallel Programming System Based on Logic	469
	Opium - A High Level Debugging Environment	472
	An Inductive Theorem Prover Based on Narrowing	475
	A Cooperative Answering System	478
	MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions	481
	ProPre. A Programming Language with Proofs	484
	FRIENDLY-WAM: An Interactive Tool to Understand the Compilation of Prolog	487
	SEPIA: A Basis for Prolog Extensions	490
	The External Database in SICStus Prolog	493
	The KCM System: Speeding-up Logic Programming Through Hardware Support	496
	Logician's Workbench	499
	EUODHILOS: A General Reasoning System for a Variety of Logics	501
	The EKS-VI System	504
	CHIP and Propia	507