The philosophy of automated theorem proving
Francis Jeffry Pelletier · 1991
Different researchers use "the philosophy of automated theorem proving " to cover different concepts, indeed, different levels of concepts. Some would count such issues as how to efficiently index databases as part of the philosophy of automated theorem proving. Others wonder about whether formulas should be represented as strings or as trees or as lists, and call this part of the philosophy of automated theorem proving. Yet others concern themselves with what kind of search should be embodied in any 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 "better", and call this a part of the philosophy of automated theorem proving. Some people wonder whether automated theorem proving should be "human oriented " or