Automated Deduction: Proof Systems and Inference Techniques
My research in the area of automated deduction aims at the development automatic proof search procedures for classical and non-classical logics. Together with former students from the Technical University of Darmstadt I work on proof search methods based on matrix-characterizations of logical validity, a very compact representation of the search space.   We have developed a uniform proof search procedure for classical logic, intuitionistic logic, various modal logics, fragments of linear logic, and induction. We have also developed a uniform algorithm for transforming the machine-found matrix proofs into sequent proofs, which enables us guide the development of proofs in interactive assistants such as Nuprl. Most of my publications in the area of Automated Deduction are available online in postscript or PDF format. An abstract with a complete reference and corresponding bibtex entry is also provided. Automated deduction tools can be downloaded from this page. A list of related web pages is given to simplify cross references.
Back to main page		Related Sites Proof Systems Research Groups People Conferences / Journals Misc. Nuprl ftp Nuprl 5 Nuprl Primitives MetaPRL   CVS HOL   Docu   Primer Coq PVS Maude Gandalf EQP ACL2 SVC ileanTAP ELF    Twelf Isabelle   Source Proof General Son of BirdBrain GQML: Modal Logics Prover TPTP L I N K NuSMV SVC STeP Bugzilla Intellektik, Darmstadt AR, TU München NuPRL (Cornell) MPI, Prog Logics DFKI Saarbrücken DAI Edinburgh CompuLog Dresden arXiv CoFI CoRR HELM OpenMath OMDOC Linear Logic Pages Metatheory and reflection David Basin Alan Bundy Roy Dyckhoff Didier Galmiche J Moore Robert Harper Dieter Hutter Heiko Mantel Jens Otten Lawrence Paulson Frank Pfenning Brigitte Pientka Benjamin Pierce John Rushby Stephan Schmitt Mark-Oliver Stehr Tanel Tammet CADE TABLEAUX FTP CL 2000, Deduction Dagstuhl Conferences ALL Conferences J.IGPL J.UCS JSC Editor Page Studia Logica I&C   related Logic Journals Forschungsführer KI Deduction USA Nuprl Publications The NuPRL book Haskell Pretty Printer

---

	The ILTP Problem Library for Intuitionistic Logic Journal of Automated Reasoning, 2006.
	Automating Proofs in Category Theory IJCAR-2006, 2006.
	Innovations in Computational Type Theory using Nuprl Journal of Applied Logic, 2005.
	The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic TABLEAUX-2005, 2005.
	A Matrix Characterization for Multiplicative Exponential Linear Logic Journal of Automated Reasoning, 2004.
	Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge Technical Report, Cornell University, 2003.
	MetaPRL - A Modular Logical Environment TPHOLs'03, 2003.
	A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics Technical Report, Cornell University, 2003.
	The Nuprl Proof Development System, Version 5: Reference Manual and User's Guide Technical Report, Cornell University, 2002.
	FDL: A Prototype Formal Digital Library Technical Report, Cornell University, 2002.
	JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants IJCAR 2001, 2001.
	Connection-Driven Inductive Theorem Proving Studia Logica, 2001.
	Matrix-based Inductive Theorem Proving. TABLEAUX-2000, 2000.
	The Nuprl Open Logical Environment CADE-17, 2000.
	A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems Information and Computation, 2000.
	Matrix-based Constructive Theorem Proving. In Intellectics and Computation, Kluwer, 2000.
	Automating Inductive Specification Proofs. Fundamenta Informatica, 1999.
	Connection-based Theorem Proving in Classical and Non-classical Logics. Journal of Universal Computer Science, 1999.
	Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. AISC'98, 1998.
	A Matrix Characterization for MELL. JELIA '98, 1998.
	Deleting Redundancy in Proof Reconstruction. TABLEAUX-98, 1998.
	Minimal and Complete Prefix Unification for Non-Classical Theorem Proving. Technical Report, TU Darmstadt, 1997.
	Connection-Based Proof Construction in Linear Logic CADE-14, 1997.
	Deciding Intuitionistic Propositional Logic via Translation into Classical Logic CADE-14, 1997.
	A Constructively Adequate Refutation System for Intuitionistic Logic TABLEAUX-97, 1997.
	A Uniform Proof Procedure for Classical and Non-classical Logics. KI-96, 1996.
	Problem-Oriented Applications of Automated Theorem Proving. DISCO '96, 1996.
	Converting Non-Classical Matrix Proofs into Sequent-Style Systems. CADE-13, 1996.
	T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. TABLEAUX-96, 1996.
	Guiding Program Development Systems by a Connection Based Proof Strategy. LoPSTr'95, 1996.
	Integrating a Connection Based Proof Method into an Interactive Program Development System. ProCos Workshop on Linking Theories, 1995.
	On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs. TABLEAUX-95, 1995.
	A Connection Based Proof Method for Intuitionistic Logic. TABLEAUX-95, 1995.
	On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs.     TABLEAUX-95, Short Papers, 1995.
	Building proofs by Analogy via the Curry-Howard Isomorphism. LPAR '92, 1992.
	Constructive automata theory implemented with the NuPRL proof development system. Technical Report, Cornell University, 1986
Back to main page