Automated deduction : CADE-11 : 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992 : proceedings
This volume contains the papers presented at the Eleventh International Conference on Automated Deduction (CADE-11) held in Saratoga Springs, NY, inJune 1992. A total of 136 papers were submitted for presentation by researchers from nearly 20 countries. Papers covered many topics including: resoluti...
Salvato in:
| Autore principale: | |
|---|---|
| Ente Autore: | |
| Natura: | Livre numérique |
| Lingua: | Anglais |
| Pubblicazione: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serie: | Lecture notes in computer science. Lecture notes in artificial intelligence
607 |
| Soggetti: | |
| Accesso online: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Automated deduction CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, proceedings, D. Kapur (Ed.), Berlin, Springer-Verlag, 1992, 1 vol. (XV-793 p.), Lecture notes in computer science, 3-540-55602-8 • Automated Deduction - CADE-11, Texte imprimé, 9783662211090 |
Sommario:
- 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 prooftransformation
- 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 KIVsystem: 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.