| 2001 | A Computer Environment for Writing Ordinary Mathematical Proofs. David McMath, Marianna Rozenfeld, Richard Sommer |
| 2001 | A Local System for Classical Logic. Kai Brünnler, Alwen Fernanto Tiu |
| 2001 | A Monotonic Higher-Order Semantic Path Ordering. Cristina Borralleras, Albert Rubio |
| 2001 | A Refinement Theory that Supports Reasoning About Knowledge and Time. Kai Engelhardt, Ron van der Meyden, Yoram Moses |
| 2001 | A Type-Theoretic Approach to Induction with Higher-Order Encodings. Carsten Schürmann |
| 2001 | Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. Jan-Georg Smaus |
| 2001 | Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search. Rong Yang, Steve Gregory |
| 2001 | Automated Proof Support for Interval Logics. Thomas Marthedal Rasmussen |
| 2001 | Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux. Reinhold Letz, Gernot Stenz |
| 2001 | Binding-Time Annotations Without Binding-Time Analysis. Wim Vanhoof, Maurice Bruynooghe |
| 2001 | Boolean Functions for Finite-Tree Dependencies. Roberto Bagnara, Enea Zaffanella, Roberta Gori, Patricia M. Hill |
| 2001 | Census Data Repair: a Challenging Application of Disjunctive Logic Programming. Enrico Franconi, Antonio Laureti Palma, Nicola Leone, Simona Perri, Francesco Scarcello |
| 2001 | Certifying Synchrony for Free. Sylvain Boulmé, Grégoire Hamon |
| 2001 | Coherence and Transitivity in Coercive Subtyping. Yong Luo, Zhaohui Luo |
| 2001 | Coherent Composition of Distributed Knowledge-Bases Through Abduction. Ofer Arieli, Bert Van Nuffelen, Marc Denecker, Maurice Bruynooghe |
| 2001 | Complexity of Linear Standard Theories. Christopher Lynch, Barbara Morawska |
| 2001 | Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2001 | Concept Formation via Proof Planning Failure. Raúl Monroy |
| 2001 | Counting the Number of Equivalent Binary Resolution Proofs. Joseph D. Horton |
| 2001 | Efficient Computation of the Well-Founded Model Using Update Propagation. Andreas Behrend |
| 2001 | Efficient Negation Using Abstract Interpretation. Susana Muñoz-Hernández, Juan José Moreno-Navarro, Manuel V. Hermenegildo |
| 2001 | First-Order Atom Definitions Extended. Bijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach |
| 2001 | Functional Logic Programming with Failure: A Set-Oriented View. Francisco Javier López-Fraguas, Jaime Sánchez-Hernández |
| 2001 | Games and Model Checking for Guarded Logics. Dietmar Berwanger, Erich Grädel |
| 2001 | Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving. Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller |
| 2001 | How to Transform an Analyzer into a Verifier. Marco Comini, Roberta Gori, Giorgio Levi |
| 2001 | Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy. Klaus Schneider |
| 2001 | Indexed Categories and Bottom-Up Semantics of Logic Programs. Gianluca Amato, James Lipton |
| 2001 | Inference of Termination Conditions for Numerical Loops in Prolog. Alexander Serebrenik, Danny De Schreye |
| 2001 | Inferring Termination Conditions for Logic Programs Using Backwards Analysis. Samir Genaim, Michael Codish |
| 2001 | Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions. Guy Perrier |
| 2001 | Local Conditional High-Level Robot Programs. Sebastian Sardiña |
| 2001 | Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets. Volker Diekert, Paul Gastin |
| 2001 | Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings Robert Nieuwenhuis, Andrei Voronkov |
| 2001 | Logical Omniscience and the Cost of Deliberation. Natasha Alechina, Brian Logan |
| 2001 | Model Generation with Boolean Constraints. Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa |
| 2001 | Monodic fragments of first-order temporal logics: 2000-2001 A.D. Ian M. Hodkinson, Frank Wolter, Michael Zakharyaschev |
| 2001 | On Bounded Specifications. Orna Kupferman, Moshe Y. Vardi |
| 2001 | On Termination of Meta-Programs. Alexander Serebrenik, Danny De Schreye |
| 2001 | Operational Semantics for Fixed-Point Logics on Constraint Databases. Stephan Kreutzer |
| 2001 | Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae. Jussi Rintanen |
| 2001 | Permutation Problems and Channelling Constraints. Toby Walsh |
| 2001 | Reachability Analysis of Term Rewriting Systems with Timbuk. Thomas Genet, Valérie Viet Triem Tong |
| 2001 | Reasoning about Evolving Nonmonotonic Knowledge Bases. Thomas Eiter, Michael Fink, Giuliana Sabbatini, Hans Tompits |
| 2001 | Simplifying Binary Propositional Theories into Connected Components Twice as Fast. Alvaro del Val |
| 2001 | Splitting Through New Proposition Symbols. Hans de Nivelle |
| 2001 | Tableaux for Reasoning About Atomic Updates. Christian G. Fermüller, Georg Moser, Richard Zach |
| 2001 | Termination of Rewriting With Strategy Annotations. Salvador Lucas |
| 2001 | The Elog Web Extraction Language. Robert Baumgartner, Sergio Flesca, Georg Gottlob |
| 2001 | The Functions Provable by First Order Abstraction. Daniel Leivant |
| 2001 | Unification in a Description Logic with Transitive Closure of Roles. Franz Baader, Ralf Küsters |