8th International conference on automated deduction : Oxford, England, July 27 August 1, 1986 : proceedings
সংরক্ষণ করুন:
| সংস্থা লেখক: | |
|---|---|
| অন্যান্য লেখক: | |
| বিন্যাস: | Livre numérique |
| ভাষা: | Anglais |
| প্রকাশিত: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| মালা: | Lecture notes in computer science
230 |
| বিষয়গুলি: | |
| অনলাইন ব্যবহার করুন: | 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: | • 8th International conference on Automated deduction, Oxford, England, July 27-August 1, 1986, proceedings, Edited by Jörg H. Siekmann, Berlin, Springer, 1986, 1 vol. (IX-708 p.), Lecture notes in computer science, 3-540-16780-3 • 8th International Conference on Automated Deduction, Texte imprimé, 9783662198230 |
সূচিপত্রের সারণি:
- Connections and higher-order logic
- Commutation, transformation, and termination
- Full-commutation and fair-termination in equational (and combined) term-rewriting systems
- An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations
- Proving termination of associative commutative rewriting systems by rewriting
- Relating resolution and algebraic completion for Horn logic
- A simple non-termination test for the Knuth-Bendix method
- A new formula for the execution of categorical combinators
- Proof by induction using test sets
- How to prove equivalence of term rewriting systems without induction
- Sufficient completeness, term rewriting systems and anti-unification
- A new method for establishing refutational completeness in theorem proving
- A theory of diagnosis from first principles
- Some contributions to the logical analysis of circumscription
- Modal theorem proving
- Computational aspects of three-valued logic
- Resolution and quantified epistemic logics
- A commonsense theory of nonmonotonic reasoning
- Negative paramodulation
- The heuristics and experimental results of a new hyperparamodulation: HL-resolution
- ECR: An equality conditional resolution proof procedure
- Using narrowing to do isolation in symbolic equation solving an experiment in automated reasoning
- Formulation of induction formulas in verification of prolog programs
- Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities
- An interactive verification system based on dynamic logic
- What you always wanted to know about clause graph resolution
- Parallel theorem proving with connection graphs
- Theory links in semantic graphs
- Abstraction usinggeneralization functions
- An improvement of deduction plans: Refutation plans
- Controlling deduction with proof condensation and heuristics
- Nested resolution
- Mechanizing constructive proofs
- Implementing number theory: An experiment with Nuprl
- Parallel algorithms for term matching
- Unification in combinations of collapse-free theories with disjoint sets of function symbols
- Combination of unification algorithms
- Unification in the data structure sets
- NP-completeness of the set unification and matching problems
- Matching with distributivity
- Unification in boolean rings
- Some relationships between unification, restricted unification, and matching
- A classification of many-sorted unification problems
- Unification in many-sorted equational theories
- Classes of first order formulas under various satisfiability definitions
- Diamond formulas in the dynamic logic of recursively enumerable programs
- A prolog machine
- A prolog technology theorem prover: Implementation by an extended prolog compiler
- Paths to high-performance automated theorem proving
- Purely functional implementation of a logic
- Causes for events: Their computation and applications
- How to clear a block: Plan formation in situational logic
- Deductive synthesis of sorting programs
- The TPS theorem proving system
- Trspec: A term rewriting based system for algebraic specifications
- Highly parallel inference machine
- Automatic theorem proving in the ISDV system
- The karlsruhe induction theorem proving system
- Overview of a theorem-prover for a computational logic
- GEO-prover A geometry theorem prover developed at UT
- The markgraf karl refutation procedure (MKRP)
- The J-machine: Functional programming with combinators
- The illinois prover: A general purpose resolutiontheorem prover
- Theorem proving systems of the Formel project
- The passau RAP system: Prototyping algebraic specifications using conditional narrowing
- RRL: A rewrite rule laboratory
- A geometry theorem prover based on Buchberger's algorithm
- REVE a rewrite rule laboratory
- ITP at argonne national laboratory
- Autologic at university of victoria
- Thinker
- The KLAUS automated deduction system
- The KRIPKE automated theorem proving system
- SHD-prover at university of texas at austin.