Symposium on automatic demonstration : held at Versailles-France, December 1968
保存先:
| 団体著者: | |
|---|---|
| その他の著者: | , , , |
| フォーマット: | Livre numérique |
| 言語: | Anglais Français |
| 出版事項: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| シリーズ: | Lecture notes in mathematics
125 |
| 主題: | |
| オンライン･アクセス: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 注記: |
Textes en français ou en anglais Colloque international sur la démonstration automatique, organisé par l'Institut de recherche d'informatique et d'automatique. Autre contribution : M. Schützenberger (éditeur) Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Symposium on automatic demonstration, held at Versailles-France, December 1968, edited by M. Laudet,... D. Lacombe, L. Nolin... [et al.], 1970, Berlin, Springer-Verlag, 1 vol. (310 p.), Lecture notes in mathematics, 0-387-04914-2 • Symposium on Automatic Demonstration, Texte imprimé, 9783662170755 |
目次:
- Allocution d'ouverture
- Presentation d'un langage de formalisation des demonstrations mathematiques naturelles
- The mathematical language AUTOMATH, its usage, and some of its extensions
- Proof theory and the accuracy of computations
- Aspects du Theoreme de completude selon Herbrand
- Decision procedure for theories categorical in Alefo
- On the long-range prospects of automatic theorem-proving
- The case for using equality axioms in automatic demonstration
- Hilbert's programme and the search for automatic proof procedures
- A linear format for resolution
- Refinement theorems in resolution theory
- Definitional approach to automatic demonstration
- Heuristic interest of using metatheorems
- A proof procedure with matrix reduction
- Axiom systems in automatic theorem proving
- Constructive validity
- Paramodulation and set of support.