Table of Contents

• Program Termination Analysis by Size-Change Graphs (Abstract)Neil D. Jones. 1-4 [doi]
• SET Cardholder Registration: The Secrecy ProofsLawrence C. Paulson. 5-12 [doi]
• Algorithms, Datastructures, and other Issues in Efficient Automated DeductionAndrei Voronkov. 13-28 [doi]
• The Description Logic ALCNH::R+:: Extended with Concrete Domains: A Practically Motivated ApproachVolker Haarslev, Ralf Möller, Michael Wessel. 29-44 [doi]
• NEXPTIME-Complete Description Logics with Concrete DomainsCarsten Lutz. 45-60 [doi]
• Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description LogicsVolker Haarslev, Ralf Möller, Anni-Yasmin Turhan. 61-75 [doi]
• The Hybrid µ-CalculusUlrike Sattler, Moshe Y. Vardi. 76-91 [doi]
• The Inverse Method Implements the Automata Approach for Modal SatisfiabilityFranz Baader, Stephan Tobies. 92-106 [doi]
• Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTLRegimantas Pliuskevicius. 107-120 [doi]
• Tableaux for Temporal Description Logic with Constant DomainsCarsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev. 121-136 [doi]
• Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid DesignationSerenella Cerrito, Marta Cialdea Mayer. 137-151 [doi]
• Instructing Equational Set-Reasoning with OtterAndrea Formisano, Eugenio G. Omodeo, Marco Temperini. 152-167 [doi]
• NP-Completeness of Refutability by Literal-Once ResolutionStefan Szeider. 168-181 [doi]
• Ordered Resolution vs. Connection Graph ResolutionReiner Hähnle, Neil V. Murray, Erik Rosenthal. 182-194 [doi]
• A Model-Based Completeness Proof of Extended Narrowing and ResolutionJürgen Stuber. 195-210 [doi]
• A Resolution-Based Decision Procedure for the Two-Variable Fragment with EqualityHans de Nivelle, Ian Pratt-Hartmann. 211-225 [doi]
• Superposition and Chaining for Totally Ordered Divisible Abelian GroupsUwe Waldmann. 226-241 [doi]
• Context TreesHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela. 242-256 [doi]
• On the Evaluation of Indexing Techniques for Theorem ProvingRobert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov. 257-271 [doi]
• Preferred Extensions of Argumentation Frameworks: Query Answering and ComputationSylvie Doutre, Jérôme Mengin. 272-288 [doi]
• Bunched Logic ProgrammingPablo A. Armelín, David J. Pym. 289-304 [doi]
• A Top-Down Procedure for Disjunctive Well-Founded SemanticsKewen Wang. 305-317 [doi]
• A Second-Order Theorem Prover Applied to CircumscriptionMichael Beeson. 318-324 [doi]
• NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set SemanticsChristian Anger, Kathrin Konczak, Thomas Linke. 325-330 [doi]
• Conditional Pure Literal GraphsMarco Benedetti. 331-346 [doi]
• Evaluating Search Heuristics and Optimization Techniques in Propositional SatisfiabilityEnrico Giunchiglia, Marco Maratea, Armando Tacchella, Davide Zambonin. 347-363 [doi]
• QUBE: A System for Deciding Quantified Boolean Formulas SatisfiabilityEnrico Giunchiglia, Massimo Narizzano, Armando Tacchella. 364-369 [doi]
• System Abstract: E 0.61Stephan Schulz. 370-375 [doi]
• Vampire 1.1 (System Description)Alexandre Riazanov, Andrei Voronkov. 376-380 [doi]
• DCTP - A Disconnection Calculus Theorem Prover - System AbstractReinhold Letz, Gernot Stenz. 381-385 [doi]
• More On Implicit SyntaxMarko Luther. 386-400 [doi]
• Termination and Reduction Checking for Higher-Order Logic ProgramsBrigitte Pientka. 401-415 [doi]
• P.rex: An Interactive Proof ExplainerArmin Fiedler. 416-420 [doi]
• JProver : Integrating Connection-Based Theorem Proving into Interactive Proof AssistantsStephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin. 421-426 [doi]
• The eXtended Least Number HeuristicGilles Audemard, Laurent Henocque. 427-442 [doi]
• System Description: SCOTT-5Kahlil Hodgson, John K. Slaney. 443-447 [doi]
• Combination of Distributed Search and Multi-search in Peers-mcd.dMaria Paola Bonacina. 448-452 [doi]
• Lotrec : The Generic Tableau Prover for Modal and Description LogicsLuis Fariñas del Cerro, David Fauthoux, Olivier Gasquet, Andreas Herzig, Dominique Longin, Fabio Massacci. 453-458 [doi]
• The MODPROF Theorem ProverJens Happe. 459-463 [doi]
• A New System and Methodology for Generating Random Modal FormulaePeter F. Patel-Schneider, Roberto Sebastiani. 464-468 [doi]
• Decidable Classes of Inductive TheoremsJürgen Giesl, Deepak Kapur. 469-484 [doi]
• Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting SystemsXavier Urbain. 485-498 [doi]
• Decidability and Complexity of Finitely Closable Linear Equational TheoriesChristopher Lynch, Barbara Morawska. 499-513 [doi]
• A New Meta-complexity Theorem for Bottom-Up Logic ProgramsHarald Ganzinger, David A. McAllester. 514-528 [doi]
• Canonical Propositional Gentzen-Type SystemsArnon Avron, Iddo Lev. 529-544 [doi]
• Incremental Closure of Free Variable TableauxMartin Giese. 545-560 [doi]
• Deriving Modular Programs from Short ProofsUwe Egly, Stephan Schmitt. 561-577 [doi]
• A General Method for Using Schematizations in Automated DeductionNicolas Peltier. 578-592 [doi]
• Approximating Dependency Graphs Using Tree Automata TechniquesAart Middeldorp. 593-610 [doi]
• On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real VariablesBernard Boigelot, Sébastien Jodogne, Pierre Wolper. 611-625 [doi]
• A Sequent Calculus for First-Order Dynamic Logic with Trace ModalitiesBernhard Beckert, Steffen Schlager. 626-641 [doi]
• Flaw Detection in Formal SpecificationsWolfgang Reif, Gerhard Schellhorn, Andreas Thums. 642-657 [doi]
• CCE: Testing Ground JoinabilityJürgen Avenhaus, Bernd Löchner. 658-662 [doi]
• System Description: RDL : Rewrite and Decision Procedure LaboratoryAlessandro Armando, Luca Compagna, Silvio Ranise. 663-669 [doi]
• lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical LogicJoshua S. Hodas, Naoyuki Tamura. 670-684 [doi]
• MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural DeductionDominique Pastre. 685-689 [doi]
• Hilberticus - A Tool Deciding an Elementary Sublanguage of Set TheoryJörg Lücke. 690-695 [doi]
• STRIP: Structural Sharing for Efficient Proof-SearchDominique Larchey-Wendling, Dominique Méry, Didier Galmiche. 696-700 [doi]
• RACER System DescriptionVolker Haarslev, Ralf Möller. 701-706 [doi]