5th Conference on Automated Deduction

Inhaltsverzeichnis

• Using meta-theoretic reasoning to do algebra.
• Generating contours of integration: An application of PROLOG in symbolic computing.
• Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation.
• Proofs as descriptions of computation.
• Program synthesis from incomplete specifications.
• A system for proving equivalences of recursive programs.
• Variable elimination and chaining in a resolution-based prover for inequalities.
• Decision procedures for some fragments of set theory.
• Simplifying interpreted formulas.
• Specification and verification of real-time, distributed systems using the theory of constraints.
• Reasoning by plausible inference.
• Logical support in a time-varying model.
• An experiment with the Boyer-Moore theorem prover: A proof of the correctness of a simple parser of expressions.
• An experiment with „Edinburgh LCF“.
• An approach to theorem proving on the basis of a typed lambda-calculus.
• Adding dynamic paramodulation to rewrite algorithms.
• Hyperparamodulation: A refinement of paramodulation.
• The AFFIRM theorem prover: Proof forests and management of large proofs.
• Data structures and control architecture for implementation of theorem-proving programs.
• A note on resolution: How to get rid of factoring without loosing completeness.
• Abstraction mappings in mechanical theorem proving.
• Transforming matings into natural deduction proofs.
• Analysis of dependencies to improve the behaviour of logic programs.
• Selective backtracking for logic programs.
• Canonical forms and unification.
• Deciding unique termination of permutative rewriting systems: Choose your term algebra carefully.
• How to prove algebraic inductive hypotheses without induction.
• A complete, nonredundant algorithm for reversed skolemization.