Logic Programming and Automated Reasoning

Soundness and completeness of partial deductions for well-founded semantics.- On deductive planning and the frame problem.- On resolution in fragments of classical linear logic (extended abstract).- A procedure for automatic proof nets construction.- Free logic and infinite constraint networks.- Towards probabilistic knowledge bases.- Two-level grammar: A functional/logic query language for database and knowledge-base systems.- Extending deductive database languages by embedded implications.- Controlling redundancy in large search spaces: Argonne-style theorem proving through the years.- Resolution for many-valued logics.- An ordered theory resolution calculus.- Application of automated deduction to the search for single axioms for exponent groups.- Elementary lower bounds for the lengths of refutations.- Shortening proofs by quantifier introduction.- Reform compilation for nonlinear recursion.- Pruning infinite failure branches in programs with occur-check.- The use of planning critics in mechanizing inductive proofs.- ??-Calculus: An algorithmic interpretation of classical natural deduction.- Building proofs by analogy via the Curry-Howard Isomorphism.- On the use of the constructive omega-rule within automated deduction.- OR-parallel theorem proving with random competition.- Parallel computation of multiple sets-of-support.- Towards using the Andorra Kernel Language for industrial real-time applications.- Unification in a combination of equational theories with shared constants and its application to primal algebras.- Non-clausal resolution and superposition with selection and redundancy criteria.- Relating innermost, weak, uniform and modular termination of term rewriting systems.- A two steps semantics for logic programs with negation.- Generalized negation asfailure and semantics of normal disjunctive logic programs.- General model theoretic semantics for Higher-Order horn logic programming.- Disjunctive deductive databases.- Netlog - A concept oriented logic programming language.- From the past to the future: Executing temporal logic programs.- Computing induction axioms.- Consistency of equational enrichments.- A programming logic for a verified structured assembly language.- The unification of infinite sets of terms and its applications.- Unification in order-sorted type theory.- Infinite, canonical string rewriting systems generated by completion.- Spes: A system for logic program transformation.- Linear Objects: A logic framework for open system programming.- ISAR: An interactive system for algebraic implementation proofs.- Mathpert: Computer support for learning algebra, trig, and calculus.- MegaLog - A platform for developing knowledge base management systems.- SPIKE, an automatic theorem prover.- An application to teaching in logic course of ATP based on natural deduction.- A generic logic environment.- ElipSys A parallel programming system based on logic.- Opium - A high-level debugging environment.- An inductive theorem prover based on narrowing.- A cooperative answering system.- MIZ-PR: A theorem prover for polymorphic and recursive functions.- ProPre A programming language with proofs.- FRIENDLY-WAM: An interactive tool to understand the compilation of PROLOG.- SEPIA - a Basis for Prolog extensions.- The external database in SICStus Prolog.- The KCM system: Speeding-up logic programming through hardware support.- Logician's Workbench.- EUODHILOS: A general reasoning system for a variety of logics.- The EKS-V1 system.- CHIP and Propia.