Conferences in DBLP
John K. Slaney The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure. [Citation Graph (0, 0)][DBLP ] Conf ] Toby Walsh A Divergence Critic. [Citation Graph (0, 0)][DBLP ] Conf ] Dieter Hutter Synthesis of Induction Orderings for Existence Proofs. [Citation Graph (0, 0)][DBLP ] Conf ] Martin Protzen Lazy Generation of Induction Hypotheses. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Plaisted The Search Efficiency of Theorem Proving Strategies. [Citation Graph (0, 0)][DBLP ] Conf ] Christophe Bourely , Ricardo Caferra , Nicolas Peltier A Method for Building Models Automatically. Experiments with an Extension of OTTER. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner , Ulrich Furbach Model Elimination Without Contrapositives. [Citation Graph (0, 0)][DBLP ] Conf ] François Bronsard , Uday S. Reddy , Robert W. Hasker Induction using Term Orderings. [Citation Graph (0, 0)][DBLP ] Conf ] Jacques Chazarain , Emmanuel Kounalis Mechanizable Inductive Proofs for a Class of Forall Exists Formulas. [Citation Graph (0, 0)][DBLP ] Conf ] Olav Lysne On the Connection between Narrowing and Proof by Consistency. [Citation Graph (0, 0)][DBLP ] Conf ] Lawrence C. Paulson A Fixedpoint Approach to Implementing (Co)Inductive Definitions. [Citation Graph (0, 0)][DBLP ] Conf ] Claus-Peter Wirth , Bernhard Gramlich On Notions of Inductive Validity for First-Oder Equational Clauses. [Citation Graph (0, 0)][DBLP ] Conf ] Siani Baker A New Application for Explanation-Based Generalisation within Automated Deduction. [Citation Graph (0, 0)][DBLP ] Conf ] Heng Chu , David A. Plaisted Semantically Guided First-Order Theorem Proving using Hyper-Linking. [Citation Graph (0, 0)][DBLP ] Conf ] D. Andre de Waal , John P. Gallagher The Applicability of Logic Program Analysis and Transformation to Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Stefan Brüning Detecting Non-Provable Goals. [Citation Graph (0, 0)][DBLP ] Conf ] Robert S. Boyer Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We? [Citation Graph (0, 0)][DBLP ] Conf ] The QED Manifesto. [Citation Graph (0, 0)][DBLP ] Conf ] Geoff Sutcliffe , Christian B. Suttner , Theodor Yemenis The TPTP Problem Library. [Citation Graph (0, 0)][DBLP ] Conf ] Eric Domenjoud , Francis Klay , Christophe Ringeissen Combination Techniques for Non-Disjoint Equational Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Gernot Salzer Primal Grammars and Unification Modulo a Binary Clause. [Citation Graph (0, 0)][DBLP ] Conf ] Koji Iwanuma Conservative Query Normalization on Parallel Circumscription. [Citation Graph (0, 0)][DBLP ] Conf ] Laurent Fribourg , Marcos Veloso Peixoto Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints. [Citation Graph (0, 0)][DBLP ] Conf ] Véronique Royer , Joachim Quantz On Intuitionistic Query Answering in Description Bases. [Citation Graph (0, 0)][DBLP ] Conf ] Mark E. Stickel , Richard J. Waldinger , Michael R. Lowry , Thomas Pressburger , Ian Underwood Deductive Composition of Astronomical Software from Subroutine Libraries. [Citation Graph (0, 0)][DBLP ] Conf ] William M. Farmer , Joshua D. Guttman , Mark E. Nadel , F. Javier Thayer Proof Script Pragmatics in IMPS. [Citation Graph (0, 0)][DBLP ] Conf ] Manfred Kerber , Michael Kohlhase A Mechanization of Strong Kleene Logic for Partial Functions. [Citation Graph (0, 0)][DBLP ] Conf ] Dongming Wang Algebraic Factoring and Geometry Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Nicholas Freitag McPhee , Shang-Ching Chou , Xiao-Shan Gao Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method. [Citation Graph (0, 0)][DBLP ] Conf ] Larry M. Hines Str+ve and Integers. [Citation Graph (0, 0)][DBLP ] Conf ] Richard Platek What is a Proof? (Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Ursula Martin Termination, Geometry and Invariants. [Citation Graph (0, 0)][DBLP ] Conf ] Leo Bachmair , Harald Ganzinger Ordered Chaining for Total Orderings. [Citation Graph (0, 0)][DBLP ] Conf ] Aart Middeldorp , Hans Zantema Simple Termination Revisited. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Basin , Toby Walsh Termination Orderings for Rippling. [Citation Graph (0, 0)][DBLP ] Conf ] David B. Sturgill , Alberto Maria Segre A Novel Asynchronous Parallelism Scheme for First-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Jean Goubault Proving with BDDs and Control of Information. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Graf Extended Path-Indexing. [Citation Graph (0, 0)][DBLP ] Conf ] Robert L. Constable Exporting and Refecting Abstract Metamathematics. [Citation Graph (0, 0)][DBLP ] Conf ] Laurent Vigneron Associative-Commutative Deduction with Constraints. [Citation Graph (0, 0)][DBLP ] Conf ] Robert Nieuwenhuis , Albert Rubio AC-Superposition with Constraints: No AC-Unifiers Needed. [Citation Graph (0, 0)][DBLP ] Conf ] Miki Hermann , Phokion G. Kolaitis The Complexity of Counting Problems in Equational Matching. [Citation Graph (0, 0)][DBLP ] Conf ] Penny Anderson Representing Proof Transformations for Program Optimizations. [Citation Graph (0, 0)][DBLP ] Conf ] Paul Jackson Exploring Abstract Algebra in Constructive Type Theory. [Citation Graph (0, 0)][DBLP ] Conf ] Amy P. Felty , Douglas J. Howe Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. [Citation Graph (0, 0)][DBLP ] Conf ] Patricia Johann , Michael Kohlhase Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. [Citation Graph (0, 0)][DBLP ] Conf ] Christian Prehofer Decidable Higher-Order Unification Problems. [Citation Graph (0, 0)][DBLP ] Conf ] Olaf Müller , Franz Weber Theory and Practice of Minimal Modular Higher-Order E-Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Rolf Socher-Ambrosius A Refined Version of General E-Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Bernhard Beckert A Completion-Based Method for Mixed Universal and Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Reinhard Bündgen On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs. [Citation Graph (0, 0)][DBLP ] Conf ] Stefan Klingenbeck , Reiner Hähnle Semantic Tableaux with Ordering Restrictions. [Citation Graph (0, 0)][DBLP ] Conf ] Fabio Massacci Strongly Analytic Tableaux for Normal Modal Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Xiaorong Huang Reconstruction Proofs at the Assertion Level. [Citation Graph (0, 0)][DBLP ] Conf ] Jian Zhang Problems on the Generation of Finite Models. [Citation Graph (0, 0)][DBLP ] Conf ] Edmund M. Clarke , Xudong Zhao Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. [Citation Graph (0, 0)][DBLP ] Conf ] John K. Slaney , Ewing L. Lusk , William McCune SCOTT: Semantically Constrained Otter System Description. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner , Ulrich Furbach PROTEIN: A PROver with a Theory Extension INterface. [Citation Graph (0, 0)][DBLP ] Conf ] Johann Schumann DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Goller , Reinhold Letz , Klaus Mayr , Johann Schumann SETHEO V3.2: Recent Developments - System Abstract. [Citation Graph (0, 0)][DBLP ] Conf ] Wolfgang Bibel , Stefan Brüning , Uwe Egly , Thomas Rath KoMeT. [Citation Graph (0, 0)][DBLP ] Conf ] Xiaorong Huang , Manfred Kerber , Michael Kohlhase , Erica Melis , Dan Nesmith , Jörn Richts , Jörg H. Siekmann Omega-MKRP: A Proof Development Environment. [Citation Graph (0, 0)][DBLP ] Conf ] Bernhard Beckert , Joachim Posegga leanTA P: Lean Tableau-Based Theorem Proving (Extended Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] John K. Slaney FINDER: Finite Domain Enumerator - System Description. [Citation Graph (0, 0)][DBLP ] Conf ] Frederic D. Portoraro Symlog: Automated Advice in Fitch-style Proof Construction. [Citation Graph (0, 0)][DBLP ] Conf ] Xiaorong Huang , Manfred Kerber , Michael Kohlhase , Erica Melis , Dan Nesmith , Jörn Richts , Jörg H. Siekmann KEIM: A Toolkit for Automated Deduction. [Citation Graph (0, 0)][DBLP ] Conf ] Frank Pfenning Elf: A Meta-Language for Deductive Systems (System Descrition). [Citation Graph (0, 0)][DBLP ] Conf ] Takeshi Ohtani , Hajime Sawamura , Toshiro Minami EUODHILOS-II on Top of GNU Epoch. [Citation Graph (0, 0)][DBLP ] Conf ] Lars-Henrik Eriksson Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions. [Citation Graph (0, 0)][DBLP ] Conf ] Bradley L. Richards , Ina Kraan , Alan Smaill , Geraint A. Wiggins Mollusc: A General Proof-Development Shell for Sequent-Based Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Tie-Cheng Wang , Allen Goldberg KITP-93: An Automated Inference System for Program Analysis. [Citation Graph (0, 0)][DBLP ] Conf ] Adel Bouhoula SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs. [Citation Graph (0, 0)][DBLP ] Conf ] Maria Paola Bonacina , William McCune Distributed Theorem Proving by Peers. [Citation Graph (0, 0)][DBLP ] Conf ] 