Automated Deduction - Cade-11: 11th International Conference on Automated Deduction, Saratoga Springs, Ny, Usa, June 15-18, 1992. Proceedings

ISBN-13: 9783540556022 / Angielski / Miękka / 1992 / 800 str.

Deepak Kapur

Opis

This volume contains the papers presented at the 11th International Conference on Automated Deduction (CADE-11) held in Saratoga Springs, New York, in June 1992. Topics covered include: resolution; term writing; natural deduction; parallel theorem provers; and unification theory.

Spis treści

The impossibility of the automation of logical reasoning.- Automatic proofs in mathematical logic and analysis.- Proving geometry statements of constructive type.- The central variable strategy of str?ve.- Unification in the union of disjoint equational theories: Combining decision procedures.- Reduction and unification in Lambda calculi with subtypes.- A combinatory logic approach to higher-order E-unification (extended abstract).- Cycle unification.- A parallel completion procedure for term rewriting systems.- Grammar rewriting.- Polynomial interpretations and the complexity of algorithms.- Uniform traversal combinators: Definition, use and properties.- Sorted unification using set constraints.- An abstract view of sorted unification.- Unification in order-sorted algebras with overloading.- Puzzles and paradoxes.- Experiments in automated deduction with condensed detachment.- Caching and lemmaizing in model elimination theorem provers.- LIM+ challenge problems by RUE hyper-resolution.- Computing prime implicates incrementally.- Linear-input subset analysis.- Theoretical study of symmetries in propositional calculus and applications.- Difference matching.- Using middle-out reasoning to control the synthesis of tail-recursive programs.- The use of proof plans to sum series.- Disproving conjectures.- An interval-based temporal logic in a multivalued setting.- A normal form for first-order temporal formulae.- Semantic entailment in non classical logics based on proofs found in classical logic.- Embedding negation as failure into a model generation theorem prover.- Automated correctness proofs of machine code programs for a commercial microprocessor.- Proving the Chinese remainder theorem by the cover set induction.- Automatic program optimization through proof transformation.- Proof search theory and practice in the (former) USSR (Tentative).- Basic paramodulation and superposition.- Theorem proving with ordering constrained clauses.- The special-relation rules are incomplete.- An improved method for adding equality to free variable semantic tableaux.- Proof search in the intuitionistic sequent calculus.- Implementing the meta-theory of deductive systems.- Tactic-based theorem proving and knowledge-based forward chaining: An experiment with Nuprl and Ontic.- Little theories.- Some termination criteria for narrowing and E-narrowing.- Decidable matching for convergent systems.- Free sequentially in orthogonal order-sorted rewriting systems with constructors.- Programming with equations: A framework for lazy parallel evaluation.- A many sorted logic with possibly empty sorts.- Theorem proving in non-standard logics based on the inverse method.- One more logic with uncertainty and resolution principle for it.- A natural deduction automated theorem proving system.- Isabelle-91.- The semantically guided linear deduction system.- The Shunyata system.- A geometry theorem prover for macintoshes.- FRI: Failure-resistant induction in RRL.- Herky: High performance rewriting in RRL.- IMPS: System description.- Proving equality theorems with hyper-linking.- Xpnet: A graphical interface to proof nets with an efficient proof checker.- &: Automated natural deduction.- An overview of Frapps 2.0: A framework for resolution-based automated proof procedure systems.- The GAZER theorem prover.- ROO: A parallel theorem prover.- RVF: An automated formal verification system.- KPROP — An AND-parallel theorem prover for propositional logic implemented in KL1 system abstract.- A report on ICL HOL.- PVS: A prototype verification system.- The KIV system: Systematic construction of verified software.- The tableau-based theorem prover 3 T A P for multiple-valued logics.- Analytica — A theorem prover in mathematica.- The FAUST — prover.- Eves system description.- MGTP: A parallel theorem prover based on lazy model generation.- Benchmark problems in which equality plays the major role.- Computing transitivity tables: A challenge for automated theorem provers.