Cargando…
A many-sorted calculus based on resolution and paramodulation
A Many-Sorted Calculus Based on Resolution and Paramodulation emphasizes the utilization of advantages and concepts of many-sorted logic for resolution and paramodulation based automated theorem proving.This book considers some first-order calculus that defines how theorems from given hypotheses by...
| Autor principal: | |
|---|---|
| Lenguaje: | eng |
| Publicado: |
Morgan Kaufmann
1987
|
| Materias: | |
| Acceso en línea: | http://cds.cern.ch/record/2031772 |
| _version_ | 1780947480064557056 |
|---|---|
| author | Walther, Christoph |
| author_facet | Walther, Christoph |
| author_sort | Walther, Christoph |
| collection | CERN |
| description | A Many-Sorted Calculus Based on Resolution and Paramodulation emphasizes the utilization of advantages and concepts of many-sorted logic for resolution and paramodulation based automated theorem proving.This book considers some first-order calculus that defines how theorems from given hypotheses by pure syntactic reasoning are obtained, shifting all the semantic and implicit argumentation to the syntactic and explicit level of formal first-order reasoning. This text discusses the efficiency of many-sorted reasoning, formal preliminaries for the RP- and ?RP-calculus, and many-sorted term rewrit |
| id | cern-2031772 |
| institution | Organización Europea para la Investigación Nuclear |
| language | eng |
| publishDate | 1987 |
| publisher | Morgan Kaufmann |
| record_format | invenio |
| spelling | cern-20317722021-04-21T20:10:51Zhttp://cds.cern.ch/record/2031772engWalther, ChristophA many-sorted calculus based on resolution and paramodulationMathematical Physics and MathematicsA Many-Sorted Calculus Based on Resolution and Paramodulation emphasizes the utilization of advantages and concepts of many-sorted logic for resolution and paramodulation based automated theorem proving.This book considers some first-order calculus that defines how theorems from given hypotheses by pure syntactic reasoning are obtained, shifting all the semantic and implicit argumentation to the syntactic and explicit level of formal first-order reasoning. This text discusses the efficiency of many-sorted reasoning, formal preliminaries for the RP- and ?RP-calculus, and many-sorted term rewritMorgan Kaufmannoai:cds.cern.ch:20317721987 |
| spellingShingle | Mathematical Physics and Mathematics Walther, Christoph A many-sorted calculus based on resolution and paramodulation |
| title | A many-sorted calculus based on resolution and paramodulation |
| title_full | A many-sorted calculus based on resolution and paramodulation |
| title_fullStr | A many-sorted calculus based on resolution and paramodulation |
| title_full_unstemmed | A many-sorted calculus based on resolution and paramodulation |
| title_short | A many-sorted calculus based on resolution and paramodulation |
| title_sort | many-sorted calculus based on resolution and paramodulation |
| topic | Mathematical Physics and Mathematics |
| url | http://cds.cern.ch/record/2031772 |
| work_keys_str_mv | AT waltherchristoph amanysortedcalculusbasedonresolutionandparamodulation AT waltherchristoph manysortedcalculusbasedonresolutionandparamodulation |