Automated Deduction - Cade-13: 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996. Proceedings 1996 ed. [Mīkstie vāki]

Saturation-based theorem proving: Past successes and future potential.-
A resolution theorem prover for intuitionistic logic.- Proof-terms for
classical and intuitionistic resolution.- Proof-search in intuitionistic
logic with equality, or back to simultaneous rigid E-unification.- Extensions
to a generalization critic for inductive proof.- Learning domain knowledge to
improve theorem proving.- Patching faulty conjectures.- Internal analogy in
theorem proving.- Termination of theorem proving by reuse.- Termination of
algorithms over non-freely generated data types.- ABSFOL: A proof checker
with abstraction.- SPASS & FLOTTER version 0.42.- The design of the CADE-13
ATP system competition.- SCANElimination of predicate quantifiers.- GEOTHER:
A geometry theorem prover.- Structuring metatheory on inductive definitions.-
An embedding of Ruby in Isabelle.- Mechanical verification of mutually
recursive procedures.- FasTraC a decentralized traffic control system based
on logic programming.- Presenting machine-found proofs.- MUltlog 1.0: Towards
an expert system for many-valued logics.- CtCoq: A system presentation.- An
introduction to geometry expert.- SiCoTHEO: Simple competitive parallel
theorem provers.- What can we hope to achieve from automated deduction?.-
Unification algorithms cannot be combined in polynomial time.- Unification
and matching modulo nilpotence.- An improved lower bound for the elementary
theories of trees.- INKA: The next generation.- XRay: A prolog technology
theorem prover for default reasoning: A system description.- IMPS: An updated
system description.- The tableau-based theorem prover 3 T A P Version 4.0.-
System description generating models by SEM.- Optimizing proof search in
model elimination.- An abstract machine for fixed-order dynamicallystratified
programs.- Unification in pseudo-linear sort theories is decidable.- Theorem
proving with group presentations: Examples and questions.- Transforming
termination by self-labelling.- Theorem proving in cancellative abelian
monoids (extended abstract).- On the practical value of different
definitional translations to normal form.- Converting non-classical matrix
proofs into sequent-style systems.- Efficient model generation through
compilation.- Algebra and automated deduction.- On Shostak's decision
procedure for combinations of theories.- Ground resolution with group
computations on semantic symmetries.- A new method for knowledge compilation:
The achievement by cycle search.- Rewrite semantics for production rule
systems: Theory and applications.- Experiments in the heuristic use of past
proof experience.- Lemma discovery in automating induction.- Advanced
indexing operations on substitution trees.- Semantic trees revisited: Some
new completeness results.- Building decision procedures for modal logics from
propositional decision procedures The case study of modal K.-
Resolution-based calculi for modal and temporal logics.- Tableaux and
algorithms for Propositional Dynamic Logic with Converse.- Reflection of
formal tactics in a deductive reflection framework.- Walther recursion.-
Proof search with set variable instantiation in the Calculus of
Constructions.- Search strategies for resolution in temporal logics.- Optimal
axiomatizations for multiple-valued operators and quantifiers based on
semi-lattices.- Grammar specification in categorial logics and theorem
proving.- Path indexing for AC-theories.- More Church-Rosser proofs (in
Isabelle/HOL).- Partitioning methods for satisfiability testing on large
formulas.