Abstract is missing.
- What Do We Know When We Know That a Theory Is Consistent?Gilles Dowek. 1-6 [doi]
- Reflecting Proofs in First-Order Logic with EqualityEvelyne Contejean, Pierre Corbineau. 7-22 [doi]
- Reasoning in Extensional Type Theory with EqualityChad E. Brown. 23-37 [doi]
- Nominal Techniques in Isabelle/HOLChristian Urban, Christine Tasson. 38-53 [doi]
- Tabling for Higher-Order Logic ProgrammingBrigitte Pientka. 54-68 [doi]
- A Focusing Inverse Method Theorem Prover for First-Order Linear LogicKaustuv Chaudhuri, Frank Pfenning. 69-83 [doi]
- The CoRe CalculusSerge Autexier. 84-98 [doi]
- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data StructuresTal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, S. Srivastava, Greta Yorsh. 99-115 [doi]
- Privacy-Sensitive Information Flow with JMLGuillaume Dufay, Amy P. Felty, Stan Matwin. 116-130 [doi]
- The Decidability of the First-Order Theory of Knuth-Bendix OrderTing Zhang, Henny B. Sipma, Zohar Manna. 131-148 [doi]
- Well-Nested Context UnificationJordi Levy, Joachim Niehren, Mateu Villaret. 149-163 [doi]
- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground RulesGuillem Godoy, Ashish Tiwari. 164-176 [doi]
- The OWL Instance Store: System DescriptionSean Bechhofer, Ian Horrocks, Daniele Turi. 177-181 [doi]
- Temporal Logics over Transitive StatesBoris Konev, Frank Wolter, Michael Zakharyaschev. 182-203 [doi]
- Deciding Monodic Fragments by Temporal ResolutionUllrich Hustadt, Boris Konev, Renate A. Schmidt. 204-218 [doi]
- Hierarchic Reasoning in Local Theory ExtensionsViorica Sofronie-Stokkermans. 219-234 [doi]
- Proof Planning for First-Order Temporal LogicClaudio Castellini, Alan Smaill. 235-249 [doi]
- System Description: Multi A Multi-strategy Proof PlannerAndreas Meier, Erica Melis. 250-254 [doi]
- Decision Procedures Customized for Formal VerificationRandal E. Bryant, Sanjit A. Seshia. 255-259 [doi]
- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger ArithmeticViktor Kuncak, Huu Hai Nguyen, Martin C. Rinard. 260-277 [doi]
- Connecting Many-Sorted TheoriesFranz Baader, Silvio Ghilardi. 278-294 [doi]
- A Proof-Producing Decision Procedure for Real ArithmeticSean McLaughlin, John Harrison. 295-314 [doi]
- The MathSAT 3 SystemMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. 315-321 [doi]
- Deduction with XOR Constraints in Security API ModellingGraham Steel. 322-336 [doi]
- On the Complexity of Equational Horn ClausesKumar Neeraj Verma, Helmut Seidl, Thomas Schwentick. 337-352 [doi]
- A Combination Method for Generating InterpolantsGreta Yorsh, Madanlal Musuvathi. 353-368 [doi]
- sKizzo: A Suite to Evaluate and Certify QBFsMarco Benedetti. 369-376 [doi]
- Regular Protocols and Attacks with Regular KnowledgeTomasz Truderung. 377-391 [doi]
- The Model Evolution Calculus with EqualityPeter Baumgartner, Cesare Tinelli. 392-408 [doi]
- Model Representation via Contexts and Implicit GeneralizationsChristian G. Fermüller, Reinhard Pichler. 409-423 [doi]
- Proving Properties of Incremental Merkle TreesMizuhito Ogawa, Eiichi Horita, Satoshi Ono. 424-440 [doi]
- Computer Search for Counterexamples to Wilkie s IdentityJian Zhang. 441-451 [doi]
- KRHyper - In Your PocketAlex Sinner, Thomas Kleemann. 452-457 [doi]