Conferences in DBLP
Harald Ganzinger Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Tanel Tammet A Resolution Theorem Prover for Intuitonistic Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Eike Ritter , David J. Pym , Lincoln A. Wallen Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Andrei Voronkov Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] Conf ] Andrew Ireland , Alan Bundy Extensions to a Generalization Critic for Inductive Proof. [Citation Graph (0, 0)][DBLP ] Conf ] Jörg Denzinger , Stephan Schulz Learning Domain Knowledge to Improve Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Martin Protzen Patching Faulty Conjectures. [Citation Graph (0, 0)][DBLP ] Conf ] Erica Melis , Jon Whittle Internal Analogy in Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Thomas Kolbe , Christoph Walther Termination of Theorem Proving by Reuse. [Citation Graph (0, 0)][DBLP ] Conf ] Claus Sengler Termination of Algorithms over Non-freely Generated Data Types. [Citation Graph (0, 0)][DBLP ] Conf ] Fausto Giunchiglia , Adolfo Villafiorita ABSFOL: A Proof Checker with Abstraction. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Weidenbach , Bernd Gaede , Georg Rock SPASS & FLOTTER Version 0.42. [Citation Graph (0, 0)][DBLP ] Conf ] Christian B. Suttner , Geoff Sutcliffe The Design of the CADE-13 ATP System Competition. [Citation Graph (0, 0)][DBLP ] Conf ] Hans Jürgen Ohlbach SCAN - Elimination of Predicate Quantifiers. [Citation Graph (0, 0)][DBLP ] Conf ] Dongming Wang GEOTHER: A Geometry Theorem Prover. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Basin , Seán Matthews Structuring Metatheory on Inductive Definitions. [Citation Graph (0, 0)][DBLP ] Conf ] Ole Rasmussen An Embedding of Ruby in Isabelle. [Citation Graph (0, 0)][DBLP ] Conf ] Peter V. Homeier , David F. Martin Mechanical Verification of Mutually Recursive Procedures. [Citation Graph (0, 0)][DBLP ] Conf ] Giovanni Felici , Giovanni Rinaldi , Klaus Truemper FasTraC: A Decentralized Traffic Control System Based on Logic Programming. [Citation Graph (0, 0)][DBLP ] Conf ] Xiaorong Huang , Armin Fiedler Presenting Machine-Found Proofs. [Citation Graph (0, 0)][DBLP ] Conf ] Matthias Baaz , Christian G. Fermüller , Gernot Salzer , Richard Zach MUltlog 1.0: Towards an Expert System for Many-Valued Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Janet Bertot , Yves Bertot CtCoq: A System Presentation. [Citation Graph (0, 0)][DBLP ] Conf ] Shang-Ching Chou , Xiao-Shan Gao , Jing-Zhong Zhang An Introduction to Geometry Expert. [Citation Graph (0, 0)][DBLP ] Conf ] Johann Schumann SiCoTHEO: Simple Competitive Parallel Theorem Provers. [Citation Graph (0, 0)][DBLP ] Conf ] Dana S. Scott What Can We Hope to Achieve From Automated Deduction? (Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Miki Hermann , Phokion G. Kolaitis Unification Algorithms Cannot be Combined in Polynomial Time. [Citation Graph (0, 0)][DBLP ] Conf ] Qing Guo , Paliath Narendran , David A. Wolfram Unification and Matching Modulo Nilpotence. [Citation Graph (0, 0)][DBLP ] Conf ] Sergei G. Vorobyov An Improved Lower Bound for the Elementary Theories of Trees. [Citation Graph (2, 0)][DBLP ] Conf ] Dieter Hutter , Claus Sengler INKA: The Next Generation. [Citation Graph (0, 0)][DBLP ] Conf ] Torsten Schaub , Stefan Brüning , Pascal Nicolas XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. [Citation Graph (0, 0)][DBLP ] Conf ] William M. Farmer , Joshua D. Guttman , F. Javier Thayer IMPS: An Updated System Description. [Citation Graph (0, 0)][DBLP ] Conf ] Bernhard Beckert , Reiner Hähnle , Peter Oel , Martin Sulzmann The Tableau-based Theorem Prover 3 TA P Version 4.0. [Citation Graph (0, 0)][DBLP ] Conf ] Jian Zhang , Hantao Zhang System Description: Generating Models by SEM. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison Optimizing Proof Search in Model Elimination. [Citation Graph (0, 0)][DBLP ] Conf ] Konstantinos F. Sagonas , Terrance Swift , David Scott Warren An Abstract Machine for Fixed-Order Dynamically Stratified Programs. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Weidenbach Unification in Pseudo-Linear Sort Theories is Decidable. [Citation Graph (0, 0)][DBLP ] Conf ] Ursula Martin Theorem Proving with Group Presentations: Examples and Questions. [Citation Graph (0, 0)][DBLP ] Conf ] Aart Middeldorp , Hitoshi Ohsaki , Hans Zantema Transforming Termination by Self-Labelling. [Citation Graph (0, 0)][DBLP ] Conf ] Harald Ganzinger , Uwe Waldmann Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Uwe Egly , Thomas Rath On the Practical Value of Different Definitional Translations to Normal Form. [Citation Graph (0, 0)][DBLP ] Conf ] Stephan Schmitt , Christoph Kreitz Converting Non-Classical Matrix Proofs into Sequent-Style Systems. [Citation Graph (0, 0)][DBLP ] Conf ] Heribert Schütz , Tim Geisler Efficient Model Generation through Compilation. [Citation Graph (0, 0)][DBLP ] Conf ] Steve Linton , Ursula Martin , Péter Pröhle , Duncan Shand Algebra and Automated Deduction. [Citation Graph (0, 0)][DBLP ] Conf ] David Cyrluk , Patrick Lincoln , Natarajan Shankar On Shostak's Decision Procedure for Combinations of Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Thierry Boy de la Tour Ground Resolution with Group Computations on Semantic Symmetries. [Citation Graph (0, 0)][DBLP ] Conf ] Olivier Roussel , Philippe Mathieu A New Method for Knowledge Compilation: The Achievement by Cycle Search. [Citation Graph (0, 0)][DBLP ] Conf ] Wayne Snyder , James G. Schmolze Rewrite Semantics for Production Rule Systems: Theory and Applications. [Citation Graph (0, 0)][DBLP ] Conf ] Matthias Fuchs Experiments in the Heuristic Use of Past Proof Experience. [Citation Graph (0, 0)][DBLP ] Conf ] Deepak Kapur , Mahadevan Subramaniam Lemma Discovery in Automated Induction. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Graf , Christoph Meyer Advanced Indexing Operations on Substitution Trees. [Citation Graph (0, 0)][DBLP ] Conf ] Christian G. Fermüller Semantic Trees Revisited: Some New Completeness Results. [Citation Graph (0, 0)][DBLP ] Conf ] Fausto Giunchiglia , Roberto Sebastiani Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. [Citation Graph (0, 0)][DBLP ] Conf ] Andreas Nonnengart Resolution-Based Calculi for Modal and Temporal Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Giuseppe De Giacomo , Fabio Massacci Tableaux and Algorithms for Propositional Dynamic Logic with Converse. [Citation Graph (0, 0)][DBLP ] Conf ] Harald Rueß Reflection of Formal Tactics in a Deductive Reflection Framework. [Citation Graph (0, 0)][DBLP ] Conf ] David A. McAllester , Kostas Arkoudas Walther Recursion. [Citation Graph (0, 0)][DBLP ] Conf ] Amy P. Felty Proof Search with Set Variable Instantiation in the Calculus of Constructions. [Citation Graph (0, 0)][DBLP ] Conf ] Clare Dixon Search Strategies for Resolution in Temporal Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Gernot Salzer Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. [Citation Graph (0, 0)][DBLP ] Conf ] Saturnino F. Luz-Filho Grammar Specification in Categorial Logics and Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Graf Path Indexing for AC-Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Tobias Nipkow More Church-Rosser Proofs (in Isabelle/HOL). [Citation Graph (0, 0)][DBLP ] Conf ] Tai Joon Park , Allen Van Gelder Partitioning Methods for Satisfiability Testing on Large Formulas. [Citation Graph (0, 0)][DBLP ] Conf ] 