| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466349003316 |
|
|
Titolo |
6th Conference on Automated Deduction [[electronic resource] ] : New York, USA, June 7-9, 1982 / / edited by D. W. Loveland |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1982.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VII, 389 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 138 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Mathematical logic |
Mathematical Logic and Formal Languages |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
Solving open questions with an automated theorem-proving program -- STP: A mechanized logic for specification and verification -- A look at TPS -- Logic machine architecture: Kernel functions -- Logic machine architecture: Inference mechanisms -- Procedure implementation through demodulation and related tricks -- The application of Homogenization to simultaneous equations -- Meta-level inference and program verification -- An example of FOL using metatheory -- Comparison of natural deduction and locking resolution implementations -- Derived preconditions and their use in program synthesis -- Automatic construction of special purpose programs -- Deciding combinations of theories -- Exponential improvement of efficient backtracking -- Exponential improvement of exhaustive backtracking: data structure and implementation -- Intuitionistic basis for non-monotonic logic -- Knowledge retrieval as limited inference -- On indefinite databases and the closed world assumption -- Proof by matrix reduction as plan + validation -- Improvements of a tautology-testing algorithm -- Representing infinite sequences of resolvents in recursive First-Order Horn Databases -- The power of the Church-Rosser property for string rewriting systems -- Universal unification and a classification of equational theories. |
|
|
|
|
|
|
|
| |