Conferences in DBLP
Edmund M. Clarke SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. [Citation Graph (0, 0)][DBLP ] Conf ] José Meseguer , Miguel Palomino , Narciso Martí-Oliet Equational Abstractions. [Citation Graph (0, 0)][DBLP ] Conf ] Jürgen Giesl , Deepak Kapur Deciding Inductive Validity of Equations. [Citation Graph (0, 0)][DBLP ] Conf ] Nao Hirokawa , Aart Middeldorp Automating the Dependency Pair Method. [Citation Graph (0, 0)][DBLP ] Conf ] Konstantin Korovin , Andrei Voronkov An AC-Compatible Knuth-Bendix Order. [Citation Graph (0, 0)][DBLP ] Conf ] Carsten Lutz , Ulrike Sattler , Lidia Tendera The Complexity of Finite Model Reasoning in Description Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Guoqiang Pan , Moshe Y. Vardi Optimizing a BDD-Based Modal Solver. [Citation Graph (0, 0)][DBLP ] Conf ] Jan Hladik , Ulrike Sattler A Translation of Looping Alternating Automata into Description Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Karl Crary , Susmit Sarkar Foundational Certified Code in a Metalogical Framework. [Citation Graph (0, 0)][DBLP ] Conf ] Farhad Mehta , Tobias Nipkow Proving Pointer Programs in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Dimitri Hendriks , Vincent van Oostrom adbmal [Citation Graph (0, 0)][DBLP ] Conf ] Aaron Stump Subset Types and Partial Functions. [Citation Graph (0, 0)][DBLP ] Conf ] Greg Nelson Reasoning about Quantifiers by Matching in the E-graph. [Citation Graph (0, 0)][DBLP ] Conf ] Sumit Gulwani , George C. Necula A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. [Citation Graph (0, 0)][DBLP ] Conf ] Harald Ganzinger , Thomas Hillenbrand , Uwe Waldmann Superposition Modulo a Shostak Theory. [Citation Graph (0, 0)][DBLP ] Conf ] Sava Krstic , Sylvain Conchon Canonization for Disjoint Unions of Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Christophe Ringeissen Matching in a Class of Combined Non-disjoint Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Johan G. F. Belinfante Reasoning about Iteration in Gödel's Class Theory. [Citation Graph (0, 0)][DBLP ] Conf ] Panagiotis Manolios , Daron Vroon Algorithms for Ordinal Arithmetic. [Citation Graph (0, 0)][DBLP ] Conf ] Arjeh M. Cohen , Scott H. Murray , Martin Pollet , Volker Sorge Certifying Solutions to Permutation Group Problems. [Citation Graph (0, 0)][DBLP ] Conf ] Ullrich Hustadt , Boris Konev TRP++2.0: A Temporal Resolution Prover. [Citation Graph (0, 0)][DBLP ] Conf ] Lucas Dixon , Jacques D. Fleuriot IsaPlanner: A Prototype Proof Planner in Isabelle. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner , Ulrich Furbach , Margret Groß-Hardt , Alex Sinner 'Living Book': -'Deduction', 'Slicing', 'Interaction'. [Citation Graph (0, 0)][DBLP ] Conf ] Simon Colton , Sophie Huczynska The Homer System. [Citation Graph (0, 0)][DBLP ] Conf ] Geoff Sutcliffe , Christian B. Suttner The CADE-19 ATP System Competition. [Citation Graph (0, 0)][DBLP ] Conf ] Eric Deplagne , Claude Kirchner , Hélène Kirchner , Quang Huy Nguyen Proof Search and Proof Check for Equational and Inductive Theorems. [Citation Graph (0, 0)][DBLP ] Conf ] Jean-Marie Gaillourdet , Thomas Hillenbrand , Bernd Löchner , Hendrik Spies The New WALDMEISTER Loop at Work. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Walther , Stephan Schweitzer About VeriFun. [Citation Graph (0, 0)][DBLP ] Conf ] Jürgen Avenhaus , Ulrich Kühler , Tobias Schmidt-Samoa , Claus-Peter Wirth How to Prove Inductive Theorems? QUODLIBET! [Citation Graph (0, 0)][DBLP ] Conf ] Anthony G. Cohn Reasoning about Qualitative Representations of Space and Time. [Citation Graph (0, 0)][DBLP ] Conf ] Harald Ganzinger , Jürgen Stuber Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner , Cesare Tinelli The Model Evolution Calculus. [Citation Graph (0, 0)][DBLP ] Conf ] Hans de Nivelle Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. [Citation Graph (0, 0)][DBLP ] Conf ] Alexandre Riazanov , Andrei Voronkov Efficient Instance Retrieval with Standard and Relational Path Indexing. [Citation Graph (0, 0)][DBLP ] Conf ] Anatoli Degtyarev , Michael Fisher , Boris Konev Monodic Temporal Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Renate A. Schmidt , Ullrich Hustadt A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. [Citation Graph (0, 0)][DBLP ] Conf ] Christopher Lynch Schematic Saturation for Decision and Unification Problems. [Citation Graph (0, 0)][DBLP ] Conf ] Siva Anantharaman , Paliath Narendran , Michaël Rusinowitch Unification Modulo ACU I Plus Homomorphisms/Distributivity. [Citation Graph (0, 0)][DBLP ] Conf ] Venkatesh Choppella , Christopher T. Haynes Source-Tracking Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Brigitte Pientka , Frank Pfenning Optimizing Higher-Order Pattern Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Manfred Schmidt-Schauß Decidability of Arity-Bounded Higher-Order Matching. [Citation Graph (0, 0)][DBLP ] Conf ] 