Department of Mathematics
Automated Reasoning in Predicate Logic and Set Theory using a Sequent Calculus
M. Randall Holmes
Boise State University
Abstract: A formal system for reasoning in propositional logic, predicate logic and set theory will be described, and a computer implementation of reasoning in this system will be described and demonstrated. The formal system is a sequent calculus adapted from a system appropriated from a paper of Marcel Crabbe, which incorporates a safe version of Quine's set theory New Foundations. One will not need to understand this description to understand what is going on in the talk. The computer program is an interactive proof checker rather than an automatic theorem prover: the user needs to construct the proofs of theorems (although automation in the program helps with organization of proofs); the role of the prover is to check the validity of the proof steps proposed by the user and display what remains to be proved after each step.
All interested persons are welcome.
The talk will be accessible to upper class students.