Online research in philosophy

Charting a "middle way" between the extremes represented by Alvin Plantinga and Richard Swinburne, Garth Hallett explores the thesis that if belief in other minds is rational and true (as it surely is), so too is belief in God. He makes a strong case that when this parity claim is appropriately restricted to a single, sound other-minds belief, belief in God and belief in other minds do prove epistemically comparable. This result, and the distinctive path that leads to it, will interest students and scholars in philosophy of religion and theology.

In this paper we review some problems with traditional approaches for acquiring and representing knowledge in the context of developing user interfaces. Methodological implications for knowledge engineering and for human-computer interaction are studied. It turns out that in order to achieve the goal of developing human-oriented (in contrast to technology-oriented) human-computer interfaces developers have to develop sound knowledge of the structure and the representational dynamics of the cognitive system which is interacting with the computer.We show that in a first step it is necessary to study and investigate the different levels and forms of representation that are involved in the interaction processes between computers and human cognitive systems. Only if designers have achieved some understanding about these representational mechanisms, user interfaces enabling individual experiences and skill development can be designed. In this paper we review mechanisms and processes for knowledge representation on a conceptual, epistemological, and methodologieal level, and sketch some ways out of the identified dilemmas for cognitive modeling in the domain of human-computer interaction.

Preface -- Introduction -- There is only one reality -- The ultimate perspective and the ultimate drama -- Proof #1: Science -- Proof #2: History -- Proof #3: Prophecy -- Proof #4: Supernatural -- Proof #5: Psychology -- Proof #6: Sociology -- Proof #7: Inerrancy -- Proof #8: Micro-science -- Proof #9: Logic -- Proof #10: The only provably -- Inerrant, complete system -- Why proof is important -- Personal iplications of proof.

Quassim Cassam has recently defended a perceptual model of knowledge of other minds: one on which we can see and thereby know that another thinks and feels. In the course of defending this model, he addresses issues about our ability to think about other minds. I argue that his solution to this 'conceptual problem' does not work. A solution to the conceptual problem is necessary if we wish to explain knowledge of other minds.

This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.

Computer science is an engineering science whose objective is to determine how to best control interactions among computational objects. We argue that it is a fundamental computer science value to design computational objects so that the dependencies required by their interactions do not result in couplings, since coupling inhibits change. The nature of knowledge in any science is revealed by how concepts in that science change through paradigm shifts, so we analyze classic paradigm shifts in both natural and computer science in terms of decoupling. We show that decoupling pervades computer science both at its core and in the wider context of computing at large, and lies at the very heart of computer science’s value system.

mathematicians for over 60 years. Amazingly, the Argonne team's automated theorem-proving program EQP took only 8 days to find a proof of it. Unfortunately, the proof found by EQP is quite complex and difficult to follow. Some of the steps of the EQP proof require highly complex and unintuitive substitution strategies. As a result, it is nearly impossible to reconstruct or verify the computer proof of the Robbins conjecture entirely by hand. This is where the unique symbolic capabilities of Mathematica 3 come in handy. With the help of Mathematica, it is relatively easy to work out and explain each step of the dense EQP proof in detail. In this paper, I use Mathematica to provide a detailed, step-by-step reconstruction of the highly complex EQP proof of the Robbins conjecture.

Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural logics. The book can also be used as an introduction to these logical systems form a procedural perspective. Readership: Computer scientists, mathematicians and philosophers, and anyone interested in the automation of reasoning based on non-classical logics. The book is suitable for self study, its only prerequisite being some elementary knowledge of logic and proof theory.

This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that the two introductory articles come first; these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science.

The computer played an essential role in the proof given by Kenneth Appel and Kenneth Henken of the Four-Color Theorem (4CT).1 First proposed in 1852 by Francis Guthrie, the four color problem is to determine whether four colors are sufficient to color any map on a plane so that no adjacent regions have the same color. Appel and Heken’s proof involves a lemma that a certain ‘avoidable’ set U of configurations is reducible. The proof of this critical lemma requires certain combinatorial checks which are too long to do by hand. The job was done by an IBM 370/168, using over 1200 hours of computer time. In 1977, Appel and Heken, assisted by John Koch, published the proof, and the 4CT has since been considered an established result. No one has seen the entire proof of the reducibility lemma. It was too long to print out; even if it had been, no one would be able to run through it step by step.