David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Different researchers use "the philosophy of automated theorem p r o v i n g " t o cover d i f f e r e n t concepts, indeed, different levels of concepts. Some w o u l d count such issues as h o w to e f f i c i e n t l y i n d e x databases as part of the philosophy of automated theorem p r o v i n g . Others wonder about whether f o r m u l a s should be represented as strings or as trees or as lists, and call this part of the philosophy of automated theorem p r o v i n g . Yet others concern themselves w i t h what k i n d o f search should b e embodied i n a n y automated theorem prover, or to what degree any automated theorem prover should resemble Prolog. Still others debate whether natural deduction or semantic tableaux or resolution is " b e t t e r " , a n d c a l l t h i s a part of the p h i l o s o p h y of automated theorem p r o v i n g . Some people wonder whether automated theorem p r o v i n g should be " h u m a n oriented" or "machine o r i e n t e d " — sometimes arguing about whether the internal p r o o f methods should be " h u m a n - I i k e " or not, sometimes arguing about whether the generated proof should be output in a f o r m u n d e r s t a n d a b l e by p e o p l e , and sometimes a r g u i n g a b o u t the d e s i r a b i l i t y o f h u m a n intervention in the process of constructing a proof. There are also those w h o ask such questions as whether we s h o u l d even be concerned w i t h completeness or w i t h soundness of a system, or perhaps we should instead look at very efficient (but i n c o m p l e t e ) subsystems or look at methods of generating models w h i c h might nevertheless validate invalid arguments. A n d a l l of these have been v i e w e d as issues in the philosophy of automated theorem proving. Here, I w o u l d l i k e to step back from such i m p l e m e n t - ation issues and ask: " W h a t do we really think we are doing when we w r i t e an automated theorem prover?" My reflections are perhaps idiosyncratic, but I do think that they put the different researchers* efforts into a broader perspective, and give us some k i n d of handle on w h i c h directions we ourselves m i g h t w i s h to pursue when constructing (or extending) an automated theorem proving system. A logic is defined to be (i) a vocabulary and formation rules ( w h i c h tells us w h a t strings of symbols are w e l l - formed formulas in the logic), and ( i i ) a definition of ' p r o o f in that system ( w h i c h tells us the conditions under which an arrangement of formulas in the system constitutes a proof). Historically speaking, definitions of ' p r o o f have been given in various different manners: the most c o m m o n have been H i l b e r t - s t y l e ( a x i o m a t i c ) , Gentzen-style (consecution, or sequent), F i t c h - s t y l e (natural deduction), and Beth-style (tableaux)..
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Ortrun Ibens (2002). Connection Tableau Calculi with Disjunctive Constraints. Studia Logica 70 (2):241 - 270.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Gordon Beavers (1993). Automated Theorem Proving for Łukasiewicz Logics. Studia Logica 52 (2):183 - 195.
Francis J. Pelletier (1993). Identity in Modal Logic Theorem Proving. Studia Logica 52 (2):291 - 308.
Angel Mora, Emilio Munoz Velasco & Joanna Golińska-Pilarek (2011). Implementing a Relational Theorem Prover for Modal Logic K. International Journal of Computer Mathematics 88 (9):1869-1884.
Joanna Golinska-Pilarek, Angel Mora & Emilio Munoz Velasco (2008). An ATP of a Relational Proof System for Order of Magnitude Reasoning with Negligibility, Non-Closeness and Distance. In Tu-Bao Ho & Zhi-Hua Zhou (eds.), PRICAI 2008: Trends in Artificial Intelligence. Springer 128--139.
Frederic D. Portoraro (1998). Strategic Construction of Fitch-Style Proofs. Studia Logica 60 (1):45-66.
Jeremy Avigad (2006). Mathematical Method and Proof. Synthese 153 (1):105 - 159.
Added to index2010-12-22
Total downloads8 ( #315,859 of 1,780,080 )
Recent downloads (6 months)5 ( #122,348 of 1,780,080 )
How can I increase my downloads?