Abstract is missing.
- Rewriting Logic Semantics: From Language Specifications to Formal Analysis ToolsJosé Meseguer, Grigore Rosu. 1-44 [doi]
- A Redundancy Criterion Based on Ground Reducibility by Ordered RewritingBernd Löchner. 45-59 [doi]
- Efficient Checking of Term Ordering ConstraintsAlexandre Riazanov, Andrei Voronkov. 60-74 [doi]
- Improved Modular Termination Proofs Using Dependency PairsRené Thiemann, Jürgen Giesl, Peter Schneider-Kamp. 75-90 [doi]
- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite ClosureGuillem Godoy, Ashish Tiwari. 91-106 [doi]
- Redundancy Notions for Paramodulation with Non-monotonic OrderingsMiquel Bofill, Albert Rubio. 107-121 [doi]
- A Resolution Decision Procedure for the Guarded Fragment with Transitive GuardsYevgeny Kazakov, Hans de Nivelle. 122-136 [doi]
- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive ConjecturesGraham Steel, Alan Bundy, Monika Maidl. 137-151 [doi]
- Decision Procedures for Recursive Data Structures with Integer ConstraintsTing Zhang, Henny B. Sipma, Zohar Manna. 152-167 [doi]
- Modular Proof Systems for Partial Functions with Weak EqualityHarald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann. 168-182 [doi]
- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal LogicsFranz Baader, Silvio Ghilardi, Cesare Tinelli. 183-197 [doi]
- Using Automated Theorem Provers to Certify Auto-generated Aerospace SoftwareEwen Denney, Bernd Fischer, Johann Schumann. 198-212 [doi]
- argo-lib: A Generic Platform for Decision ProceduresFilip Maric, Predrag Janicic. 213-217 [doi]
- The ICS Decision Procedures for Embedded DeductionLeonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar. 218-222 [doi]
- System Description: E 0.81Stephan Schulz. 223-228 [doi]
- Second-Order Logic over Finite Structures - Report on a Research ProgrammeGeorg Gottlob. 229-243 [doi]
- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended AbstractÀngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini. 244-258 [doi]
- PDL with Negation of Atomic ProgramsCarsten Lutz, Dirk Walther. 259-273 [doi]
- Counter-Model Search in Gödel-Dummett LogicsDominique Larchey-Wendling. 274-288 [doi]
- Generalised Handling of Variables in Disconnection TableauxReinhold Letz, Gernot Stenz. 289-306 [doi]
- Chain Resolution for the Semantic WebTanel Tammet. 307-320 [doi]
- Sonic - Non-standard Inferences Go OilEdAnni-Yasmin Turhan, Christian Kissig. 321-325 [doi]
- TeMP: A Temporal Monodic ProverUllrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov. 326-330 [doi]
- Dr.Doodle: A Diagrammatic Theorem ProverDaniel Winterstein, Alan Bundy, Corin A. Gurr. 331-335 [doi]
- Solving Constraints by Elimination MethodsVolker Weispfenning. 336-341 [doi]
- Analyzing Selected Quantified Integer ProgramsK. Subramani. 342-356 [doi]
- Formalizing O Notation in Isabelle/HOLJeremy Avigad, Kevin Donnelly. 357-371 [doi]
- Experiments on Supporting Interactive Proof Using ResolutionJia Meng, Lawrence C. Paulson. 372-384 [doi]
- A Machine-Checked Formalization of the Generic Model and the Random Oracle ModelGilles Barthe, Jan Cederquist, Sabrina Tarento. 385-399 [doi]
- Automatic Generation of Classification Theorems for Finite AlgebrasSimon Colton, Andreas Meier, Volker Sorge, Roy L. McCasland. 400-414 [doi]
- Efficient Algorithms for Computing Modulo Permutation TheoriesJürgen Avenhaus. 415-429 [doi]
- Overlapping Leaf Permutative EquationsThierry Boy de la Tour, Mnacho Echenim. 430-444 [doi]
- TaMeD: A Tableau Method for Deduction ModuloRichard Bonichon. 445-459 [doi]
- Lambda LogicMichael Beeson. 460-474 [doi]
- Formalizing Undefinedness Arising in CalculusWilliam M. Farmer. 475-489 [doi]
- The CADE ATP System CompetitionGeoff Sutcliffe, Christian B. Suttner. 490-491 [doi]