PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2006 | 9 | 22 | 31-60
Tytuł artykułu

The Present State of Mechanized Deduction, and the Present Knowledge of its Limitations

Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
The aim of the paper is to present the history of researches devoted to the mechanization of reasoning. We start by describing the early attempts of applying computers to prove theorems, in particular the results of Davis, Newell-Shaw-Simon, Gilmore, Gelentner et al., Hao Wang and Davis-Putnam are considered. Further the method of resolution and unification as well as their modifications are discussed. They turned out to be crucial for further development of researches towards mechanization and automatization of reasonings - the latter are skechted in next sections. The last section of the paper is devoted to limitations of mechanized deduction and automated theorem proving. Effective and feasible computability/decidability/deducibility are distinguished and some examples of the complexity of decision procedures for certain theories are provided. The role of the speed-up phenomenon is considered and Boolos' example indicating the strength of the second order logic is discussed.
Rocznik
Tom
9
Numer
22
Strony
31-60
Opis fizyczny
Rodzaj publikacji
ARTICLE
Twórcy
  • R. Murawski, Uniwersytet im. Adama Mickiewicza, Wydzial Matematyki i Informatyki, ul. Umultowska 87, 61-614 Poznan, Poland
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
CEJSH db identifier
07PLAAAA02224687
Identyfikator YADDA
bwmeta1.element.a6d8d9fd-017a-30ab-a500-7b09ac5c0b63
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.