9th international conference on automated deduction : Argonne, Illinois, USA, May 23 26, 1988 : proceedings
This volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place du...
保存先:
| 団体著者: | |
|---|---|
| その他の著者: | , |
| フォーマット: | Livre numérique |
| 言語: | Anglais |
| 出版事項: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| シリーズ: | Lecture notes in computer science
310 |
| 主題: | |
| オンライン･アクセス: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 注記: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, proceedings, E. Lusk, R. Overbeek (Eds.), Berlin, Springer-Verlag, 1988, 1 vol. (X-775 p.), Lecture notes in computer science, 3-540-19343-X • 9th International Conference on Automated Deduction, Texte imprimé, 9783662167793 |
目次:
- First-order theorem proving using conditional rewrite rules
- Elements of Z-module reasoning
- Learning and applying generalised solutions using higher order resolution
- Specifying theorem provers in a higher-order logic programming language
- Query processing in quantitative logic programming
- An environment for automated reasoning about partial functions
- The use of explicit plans to guide inductive proofs
- Logicalc: An environment for interactive proof development
- Implementing verification strategies in the KIV-system
- Checking natural language proofs
- Consistency of rule-based expert systems
- A mechanizable induction principle for equational specifications
- Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time
- Towards efficient "knowledge-based" automated theorem proving for non-standard logics
- Propositional temporal interval logic is PSPACE complete
- Computational metatheory in Nuprl
- Type inference in Prolog
- Procedural interpretation of non-horn logic programs
- Recursive query answering with non-horn clauses
- Case inference in resolution-based languages
- Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine
- Exploitation of parallelism in prototypical deduction problems
- A decision procedure for unquantified formulas of graph theory
- Adventures in associative-commutative unification (A summary)
- Unification in finite algebras is unitary(?)
- Unification in a combination of arbitrary disjoint equational theories
- Partial unification for graph based equational reasoning
- SATCHMO: A theorem prover implemented in Prolog
- Term rewriting: Some experimental results
- Analogical reasoning and proof discovery
- Hyper-chaining and knowledge-based theorem proving
- Linear modal deductions
- A resolution calculus for modal logics
- Solving disequations in equational theories
- On word problems in Horn theories
- Canonical conditional rewrite systems
- Program synthesis by completion with dependent subtypes
- Reasoning about systems of linear inequalities
- A subsumption algorithm based on characteristic matrices
- A restriction of factoring in binary resolution
- Supposition-based logic for automated nonmonotonic reasoning
- Argument-bounded algorithms as a basis for automated termination proofs
- Two automated methods in implementation proofs
- A new approach to universal unfication and its application to AC-unification
- An implementation of a dissolution-based system employing theory links
- Decision procedure for autoepistemic logic
- Logical matrix generation and testing
- Optimal time bounds for parallel term matching
- Challenge equality problems in lattice theory
- Single axioms in the implicational propositional calculus
- Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs
- Challenge problems from nonassociative rings for theorem provers
- An interactive enhancement to the Boyer-Moore theorem prover
- A goal directed theorem prover
- m-NEVER system summary
- EFS An interactive Environment for Formal Systems
- Ontic: A knowledge representation system for mathematics
- Some tools for an inference laboratory (ATINF)
- Quantlog: A system for approximate reasoning in inconsistent formal systems
- LP: The larch prover
- The KLAUS automated deduction system
- A Prolog technology theorem prover
- ?Prolog: An extended logic programming language
- SYMEVAL: A theorem prover based on the experimental logic
- ZPLAN: An automatic reasoning system forsituations
- The TPS theorem proving system
- MOLOG: A modal PROLOG
- PARTHENON: A parallel theorem prover for non-horn clauses
- An nH-Prolog implementation
- RRL: A rewrite rule laboratory
- Geometer: A theorem prover for algebraic geometry
- Isabelle: The next seven hundred theorem provers
- The CHIP system : Constraint handling in Prolog.