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
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


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