Logic programming and automated reasoning : international conference, LPAR '92, St. Petersburg, Russia, July 15-20, 1992 : proceedings

"This volume contains the proceedings of LPAR '92, the international conference on logic programming and automated reasoning held in St. Petersburg in July 1992. The aim of the conference was to bring together researchers from the Russian and the international logic programming and theorem proving communities. The topics of interest covered by papers inthe volume include automated theorem proving, non-monotonic reasoning, applications of mathematical logic to computer science, deductive databases, implementation of declarative concepts, and programming in non-classical logics. LPAR '92 is the successor of the First and Second Russian Conferences on Logic Programming held in 1990 and 1991, respectively, the proceedings of which were publishedin LNAI Vol. 592"--PUBLISHER'S WEBSITE Soundness and completeness of partial deductions for well-founded semantics....Pages 1-12 On deductive planning and the frame problem....Pages 13-29 On resolution in fragments of classical linear logic (extended abstract)....Pages 30-41 A procedure for automatic proof nets construction....Pages 42-53 Free logic and infinite constraint networks....Pages 54-65 Towards probabilistic knowledge bases....Pages 66-77 Two-level grammar: A functional/logic query language for database and knowledge-base systems....Pages 78-83 Extending deductive database languages by embedded implications....Pages 84-95 Controlling redundancy in large search spaces: Argonne-style theorem proving through the years....Pages 96-106 Resolution for many-valued logics....Pages 107-118 An ordered theory resolution calculus....Pages 119-130 Application of automated deduction to the search for single axioms for exponent groups....Pages 131-136 Elementary lower bounds for the lengths of refutations....Pages 137-147 Shortening proofs by quantifier introduction....Pages 148-159 Reform compilation for nonlinear recursion....Pages 160-171 Pruning infinite failure branches in programs with occur-check....Pages 172-177 The use of planning critics in mechanizing inductive proofs....Pages 178-189 λμ-Calculus: An algorithmic interpretation of classical natural deduction....Pages 190-201 Building proofs by analogy via the Curry-Howard Isomorphism....Pages 202-213 On the use of the constructive omega-rule within automated deduction....Pages 214-225 OR-parallel theorem proving with random competition....Pages 226-237 Parallel computation of multiple sets-of-support....Pages 238-249 Towards using the Andorra Kernel Language for industrial real-time applications....Pages 250-260 Unification in a combination of equational theories with shared constants and its application to primal algebras....Pages 261-272 Non-clausal resolution and superposition with selection and redundancy criteria....Pages 273-284 Relating innermost, weak, uniform and modular termination of term rewriting systems....Pages 285-296 A two steps semantics for logic programs with negation....Pages 297-308 Generalized negation as failure and semantics of normal disjunctive logic programs....Pages 309-319 General model theoretic semantics for Higher-Order horn logic programming....Pages 320-331 Disjunctive deductive databases....Pages 332-356 Netlog — A concept oriented logic programming language....Pages 357-368 From the past to the future: Executing temporal logic programs....Pages 369-380 Computing induction axioms....Pages 381-392 Consistency of equational enrichments....Pages 393-402 A programming logic for a verified structured assembly language....Pages 403-408 The unification of infinite sets of terms and its applications....Pages 409-420 Unification in order-sorted type theory....Pages 421-432 Infinite, canonical string rewriting systems generated by completion....Pages 433-444 Spes: A system for logic program transformation....Pages 445-447 Linear Objects: A logic framework for open system programming....Pages 448-450 ISAR: An interactive system for algebraic implementation proofs....Pages 451-453 Mathpert: Computer support for learning algebra, trig, and calculus....Pages 454-456 MegaLog — A platform for developing knowledge base management systems....Pages 457-459 SPIKE, an automatic theorem prover....Pages 460-462 An application to teaching in logic course of ATP based on natural deduction....Pages 463-465 A generic logic environment....Pages 466-468 ElipSys A parallel programming system based on logic....Pages 469-471 Opium — A high-level debugging environment....Pages 472-474 An inductive theorem prover based on narrowing....Pages 475-477 A cooperative answering system....Pages 478-480 MIZ-PR: A theorem prover for polymorphic and recursive functions....Pages 481-483 ProPre A programming language with proofs....Pages 484-486 FRIENDLY-WAM: An interactive tool to understand the compilation of PROLOG....Pages 487-489 SEPIA — a Basis for Prolog extensions....Pages 490-492 The external database in SICStus Prolog....Pages 493-495 The KCM system: Speeding-up logic programming through hardware support....Pages 496-498 Logician's Workbench....Pages 499-500 EUODHILOS: A general reasoning system for a variety of logics....Pages 501-503 The EKS-V1 system....Pages 504-506 CHIP and Propia....Pages 507-509

This volume contains the proceedings of LPAR '92, the international conference on logic programming and automated reasoning held in St. Petersburg in July 1992. The aim of the conference was to bring together researchers from the Russian and the international logic programming and theorem proving communities.
The topics of interest covered by papers inthe volume include automated theorem proving, non-monotonic reasoning,
applications of mathematical logic to computer science,
deductive databases, implementation of declarative concepts,
and programming in non-classical logics.
LPAR '92 is the successor of the First and Second Russian Conferences on Logic Programming held in 1990 and 1991,
respectively, the proceedings of which were publishedin LNAI Vol. 592.