7th international conference on automated deduction : Napa, California, USA May 14 16, 1984 : proceedings
The Seventh International Conference on Automated Deduction was held May 14-16, 19S4, in Napa, California. The conference is the primary forum for reporting research in all aspects of automated deduction, including the design, implementation, and applications of theorem-proving systems, knowledge re...
Gorde:
| Erakunde egilea: | |
|---|---|
| Beste egile batzuk: | |
| Formatua: | Livre numérique |
| Hizkuntza: | Anglais |
| Argitaratua: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Saila: | Lecture notes in computer science
170 |
| Gaiak: | |
| Sarrera elektronikoa: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Oharra: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • 7th international conference on Automated deduction, proceedings, Napa, California, May 14-16, 1984, Edited by R.E. Shostak, Berlin, Springer, 1984, 1 vol. (vi-508 p.), Lecture notes in computer science, 3-540-96022-8 • 7th International Conference on Automated Deduction, Texte imprimé, 9781475789249 |
Aurkibidea:
- Universal Unification
- A Portable Environment for Research in Automated Reasoning
- A Natural Proof System Based on Rewriting Techniques
- EKL A Mathematically Oriented Proof Checker
- A Linear Characterization of NP-Complete Problems
- A Satisfiability Tester for Non-Clausal Propositional Calculus
- A Decision Method for Linear Temporal Logic
- A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups
- Canonical Forms in Finitely Presented Algebras
- Term Rewriting Systems and Algebra
- Termination of a Set of Rules Modulo a Set of Equations
- Associative-Commutative Unification
- A Linear Time Algorithm for a Subcase of Second Order Instantiation
- A New Equational Unification Method: A Generalisation of Martelli-Montanari s Algorithm
- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x 3 = x Implies Ring Commutativity
- A Narrowing Procedure for Theories with Constructors
- A General Inductive Completion Algorithm and Application to Abstract Data Types
- The Next Generation of Interactive Theorem Provers
- The Linked Inference Principle, II: The User s Viewpoint
- A New Interpretation of the Resolution Principle
- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving
- Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs
- Analytic and Non-analytic Proofs
- Applications of Protected Circumscription
- Implementation Strategies for Plan-Based Deduction
- A Programming Notation for Tactical Reasoning
- The Mechanization of Existence Proofs of Recursive Predicates
- Solving Word Problems in Free Algebras Using Complexity Functions
- Solving a Problem in Relevance Logic with an Automated Theorem Prover.