Abstract is missing.
- A dynamic programming approach to categorial deductionPhilippe de Groote. 1-15 [doi]
- Tractable Transformations from Modal Provability Logics into First-Order LogicStéphane Demri, Rajeev Goré. 16-30 [doi]
- Invited Talk: Decision procedures for guarded logicsErich Grädel. 31-51 [doi]
- A PSpace Algorithm for Graded Modal LogicStephan Tobies. 52-66 [doi]
- Solvability of Context Equations with Two Context Variables is DecidableManfred Schmidt-Schauß, Klaus U. Schulz. 67-81 [doi]
- Complexity of the higher order matchingTomasz Wierzbicki. 82-96 [doi]
- Solving Equational Problems EfficientlyReinhard Pichler. 97-111 [doi]
- VSDITLU: a verifiable symbolic definite integral table look-upA. A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin. 112-126 [doi]
- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem ProversPredrag Janicic, Alan Bundy, Ian Green. 127-141 [doi]
- Presenting Proofs in a Human-Oriented WayHelmut Horacek. 142-156 [doi]
- On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity ResultsViorica Sofronie-Stokkermans. 157-171 [doi]
- Maslov s Class K RevisitedUllrich Hustadt, Renate A. Schmidt. 172-186 [doi]
- Prefixed Resolution: A Resolution Method for Modal and Description LogicsCarlos Areces, Hans de Nivelle, Maarten de Rijke. 187-201 [doi]
- System Description: Twelf - A Meta-Logical Framework for Deductive SystemsFrank Pfenning, Carsten Schürmann. 202-206 [doi]
- System Description: inka 5.0 - A Logic VoyagerSerge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer. 207-211 [doi]
- System Description: CutRes 0.1: Cut Elimination by ResolutionMatthias Baaz, Alexander Leitsch, Georg Moser. 212-216 [doi]
- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem ProvingAndreas Franke, Michael Kohlhase. 217-221 [doi]
- System Description: Using OBDD s for the validation of Skolem verification conditionsE. Pascal Gribomont, Nachaat Salloum. 222-226 [doi]
- Fault-Tolerant Distributed Theorem ProvingJason Hickey. 227-231 [doi]
- System Description: Waldmeister - Improvements in Performance and Ease of UseThomas Hillenbrand, Andreas Jaeger, Bernd Löchner. 232-236 [doi]
- Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous SystemsAmy P. Felty, Douglas J. Howe, Abhik Roychoudhury. 237-251 [doi]
- A formalization of Static Analyses in System FFrédéric Prost. 252-266 [doi]
- On Explicit Reflection in Theorem Proving and Formal VerificationSergei N. Artëmov. 267-281 [doi]
- System Description: Kimba, A Model Generator for Many-Valued First-Order LogicsKarsten Konrad, David A. Wolfram. 282-286 [doi]
- System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-PrologGopalan Nadathur, Dustin J. Mitchell. 287-291 [doi]
- VampireAlexandre Riazanov, Andrei Voronkov. 292-296 [doi]
- System Abstract: E 0.3Stephan Schulz. 297-301 [doi]
- Invited Talk: Rewrite-based Deduction and Symbolic ConstraintsRobert Nieuwenhuis. 302-313 [doi]
- Towards an Automatic Analysis of Security Protocols in First-Order LogicChristoph Weidenbach. 314-328 [doi]
- A Confluent Connection CalculusPeter Baumgartner, Norbert Eisinger, Ulrich Furbach. 329-343 [doi]
- Abstraction-Based Relevancy Testing for Model EliminationMarc Fuchs, Dirk Fuchs. 344-358 [doi]
- A Breadth-First Strategy for Mating SearchMatthew Bishop. 359-373 [doi]
- The Design of the CADE-16 Inductive Theorem Prover ContestDieter Hutter, Alan Bundy. 374-377 [doi]
- System Description: Spass Version 1.0.0Christoph Weidenbach. 378-382 [doi]
- KK: a theorem prover for KAndrei Voronkov. 383-387 [doi]
- System Description: CyNTHIAJon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe. 388-392 [doi]
- System Description: MCS: Model-based Conjecture SearchingJian Zhang. 393-397 [doi]
- Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract)Tobias Nipkow. 398 [doi]
- Extensional Higher-Order Paramodulation and RUE-ResolutionChristoph Benzmüller. 399-413 [doi]
- Automatic Generation of Proof Search Strategies for Second-order LogicRaul H. C. Lopes. 414-428 [doi]