Abstract is missing.
- SAT-Based Counterexample Guided Abstraction Refinement in Model CheckingEdmund M. Clarke. 1 [doi]
- Equational AbstractionsJosé Meseguer, Miguel Palomino, Narciso Martí-Oliet. 2-16 [doi]
- Deciding Inductive Validity of EquationsJürgen Giesl, Deepak Kapur. 17-31 [doi]
- Automating the Dependency Pair MethodNao Hirokawa, Aart Middeldorp. 32-46 [doi]
- An AC-Compatible Knuth-Bendix OrderKonstantin Korovin, Andrei Voronkov. 47-59 [doi]
- The Complexity of Finite Model Reasoning in Description LogicsCarsten Lutz, Ulrike Sattler, Lidia Tendera. 60-74 [doi]
- Optimizing a BDD-Based Modal SolverGuoqiang Pan, Moshe Y. Vardi. 75-89 [doi]
- A Translation of Looping Alternating Automata into Description LogicsJan Hladik, Ulrike Sattler. 90-105 [doi]
- Foundational Certified Code in a Metalogical FrameworkKarl Crary, Susmit Sarkar. 106-120 [doi]
- Proving Pointer Programs in Higher-Order LogicFarhad Mehta, Tobias Nipkow. 121-135 [doi]
- adbmalDimitri Hendriks, Vincent van Oostrom. 136-150 [doi]
- Subset Types and Partial FunctionsAaron Stump. 151-165 [doi]
- Reasoning about Quantifiers by Matching in the E-graphGreg Nelson. 166 [doi]
- A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function SymbolsSumit Gulwani, George C. Necula. 167-181 [doi]
- Superposition Modulo a Shostak TheoryHarald Ganzinger, Thomas Hillenbrand, Uwe Waldmann. 182-196 [doi]
- Canonization for Disjoint Unions of TheoriesSava Krstic, Sylvain Conchon. 197-211 [doi]
- Matching in a Class of Combined Non-disjoint TheoriesChristophe Ringeissen. 212-227 [doi]
- Reasoning about Iteration in Gödel s Class TheoryJohan G. F. Belinfante. 228-242 [doi]
- Algorithms for Ordinal ArithmeticPanagiotis Manolios, Daron Vroon. 243-257 [doi]
- Certifying Solutions to Permutation Group ProblemsArjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge. 258-273 [doi]
- TRP++2.0: A Temporal Resolution ProverUllrich Hustadt, Boris Konev. 274-278 [doi]
- IsaPlanner: A Prototype Proof Planner in IsabelleLucas Dixon, Jacques D. Fleuriot. 279-283 [doi]
- Living Book : - Deduction , Slicing , Interaction Peter Baumgartner, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner. 284-288 [doi]
- The Homer SystemSimon Colton, Sophie Huczynska. 289-294 [doi]
- The CADE-19 ATP System CompetitionGeoff Sutcliffe, Christian B. Suttner. 295-296 [doi]
- Proof Search and Proof Check for Equational and Inductive TheoremsEric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen. 297-316 [doi]
- The New WALDMEISTER Loop at WorkJean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies. 317-321 [doi]
- About VeriFunChristoph Walther, Stephan Schweitzer. 322-327 [doi]
- How to Prove Inductive Theorems? QUODLIBET!Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth. 328-333 [doi]
- Reasoning about Qualitative Representations of Space and TimeAnthony G. Cohn. 334 [doi]
- Superposition with Equivalence Reasoning and Delayed Clause Normal Form TransformationHarald Ganzinger, Jürgen Stuber. 335-349 [doi]
- The Model Evolution CalculusPeter Baumgartner, Cesare Tinelli. 350-364 [doi]
- Translation of Resolution Proofs into Short First-Order Proofs without Choice AxiomsHans de Nivelle. 365-379 [doi]
- Efficient Instance Retrieval with Standard and Relational Path IndexingAlexandre Riazanov, Andrei Voronkov. 380-396 [doi]
- Monodic Temporal ResolutionAnatoli Degtyarev, Michael Fisher, Boris Konev. 397-411 [doi]
- A Principle for Incorporating Axioms into the First-Order Translation of Modal FormulaeRenate A. Schmidt, Ullrich Hustadt. 412-426 [doi]
- Schematic Saturation for Decision and Unification ProblemsChristopher Lynch. 427-441 [doi]
- Unification Modulo ACU I Plus Homomorphisms/DistributivitySiva Anantharaman, Paliath Narendran, Michaël Rusinowitch. 442-457 [doi]
- Source-Tracking UnificationVenkatesh Choppella, Christopher T. Haynes. 458-472 [doi]
- Optimizing Higher-Order Pattern UnificationBrigitte Pientka, Frank Pfenning. 473-487 [doi]
- Decidability of Arity-Bounded Higher-Order MatchingManfred Schmidt-Schauß. 488-502 [doi]