Conferences in DBLP
John Harrison High-Level Verification Using Theorem Proving and Formalized Mathematics. [Citation Graph (0, 0)][DBLP ] Conf ] Neophytos G. Michael , Andrew W. Appel Machine Instruction Syntax and Semantics in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] George C. Necula , Peter Lee Proof Generation in the Touchstone Theorem Prover. [Citation Graph (0, 0)][DBLP ] Conf ] Konrad Slind Wellfounded Schematic Definitions. [Citation Graph (0, 0)][DBLP ] Conf ] Leo Bachmair , Ashish Tiwari Abstract Congruence Closure and Specializations. [Citation Graph (0, 0)][DBLP ] Conf ] Clark W. Barrett , David L. Dill , Aaron Stump A Framework for Cooperating Decision Procedures. [Citation Graph (0, 0)][DBLP ] Conf ] Florian Kammüller Modular Reasoning in Isabelle. [Citation Graph (0, 0)][DBLP ] Conf ] William M. Farmer An Infrastructure for Intertheory Reasoning. [Citation Graph (0, 0)][DBLP ] Conf ] Johan G. F. Belinfante Gödel's Algorithm for Class Formation. [Citation Graph (0, 0)][DBLP ] Conf ] Marc Bezem , Dimitri Hendriks , Hans de Nivelle Automated Proof Construction in Type Theory Using Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Peter B. Andrews , Matthew Bishop , Chad E. Brown System Description: TPS: A Theorem Proving System for Type Theory. [Citation Graph (0, 0)][DBLP ] Conf ] Stuart F. Allen , Robert L. Constable , Richard Eaton , Christoph Kreitz , Lori Lorigo The Nuprl Open Logical Environment. [Citation Graph (0, 0)][DBLP ] Conf ] Carsten Sinz System Description: ARA - An Automatic Theorem Prover for Relation Algebras. [Citation Graph (0, 0)][DBLP ] Conf ] Henry A. Kautz Scalable Knowledge Representation and Reasoning Systems. [Citation Graph (0, 0)][DBLP ] Conf ] Ryuzo Hasegawa , Hiroshi Fujita , Miyuki Koshimura Efficient Minimal Model Generation Using Branching Lemmas. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. [Citation Graph (0, 0)][DBLP ] Conf ] Ashish Tiwari , Leo Bachmair , Harald Rueß Rigid E -Unification Revisited. [Citation Graph (0, 0)][DBLP ] Conf ] Carl-Johan H. Seger Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. [Citation Graph (0, 0)][DBLP ] Conf ] E. Allen Emerson , Vineet Kahlon Reducing Model Checking of the Many to the Few. [Citation Graph (0, 0)][DBLP ] Conf ] Doron Bustan , Orna Grumberg Simulation Based Minimization. [Citation Graph (0, 0)][DBLP ] Conf ] Thomas Genet , Francis Klay Rewriting for Cryptographic Protocol Verification. [Citation Graph (0, 0)][DBLP ] Conf ] Enrico Giunchiglia , Armando Tacchella System Description: *SAT: A Platform for the Development of Modal Decision Procedures. [Citation Graph (0, 0)][DBLP ] Conf ] Peter F. Patel-Schneider System Description: DLP. [Citation Graph (0, 0)][DBLP ] Conf ] Gilles Audemard , Belaid Benhamou , Laurent Henocque Two Techniques to Improve Finite Model Search. [Citation Graph (0, 0)][DBLP ] Conf ] Jürgen Giesl , Aart Middeldorp Eliminating Dummy Elimination. [Citation Graph (0, 0)][DBLP ] Conf ] Deepak Kapur , Mahadevan Subramaniam Extending Decision Procedures with Induction Schemes. [Citation Graph (0, 0)][DBLP ] Conf ] Cristina Borralleras , Maria Ferreira , Albert Rubio Complete Monotonic Semantic Path Orderings. [Citation Graph (0, 0)][DBLP ] Conf ] Anatoli Degtyarev , Andrei Voronkov Stratified Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Bruce Spencer , Joseph Douglas Horton Support Ordered Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] William McCune , Olga Shumsky System Description: IVY. [Citation Graph (0, 0)][DBLP ] Conf ] Geoff Sutcliffe System Description: SystemOn TPTP. [Citation Graph (0, 0)][DBLP ] Conf ] Marianne Brown , Geoff Sutcliffe System Description: PTTP+GLiDes: Semantically Guided PTTP. [Citation Graph (0, 0)][DBLP ] Conf ] Guillaume Gillard A Formalization of a Concurrent Object Calculus up to alpha-Conversion. [Citation Graph (0, 0)][DBLP ] Conf ] Renate A. Schmidt , Ullrich Hustadt A Resolution Decision Procedure for Fluted Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Philippe Chatalic , Laurent Simon ZRES: The Old Davis-Putman Procedure Meets ZBDD. [Citation Graph (0, 0)][DBLP ] Conf ] Andreas Franke , Michael Kohlhase System Description: MBASE, an Open Mathematical Knowledge Base. [Citation Graph (0, 0)][DBLP ] Conf ] Andreas Meier System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. [Citation Graph (0, 0)][DBLP ] Conf ] Viorica Sofronie-Stokkermans On Unification for Bonded Distributive Lattices. [Citation Graph (0, 0)][DBLP ] Conf ] Ian Horrocks , Ulrike Sattler , Stephan Tobies Reasoning with Individuals for the Description Logic SHIQ. [Citation Graph (0, 0)][DBLP ] Conf ] Graham Collins , Louise A. Dennis System Description: Embedding Verification into Microsoft Excel. [Citation Graph (0, 0)][DBLP ] Conf ] Michael Jackson , Helen Lowe System Description: Interactive Proof Critics in XBarnacle. [Citation Graph (0, 0)][DBLP ] Conf ] Carsten Schürmann Tutorial: Meta-logical Frameworks. [Citation Graph (0, 0)][DBLP ] Conf ] Stephen G. Pulman Tutorial: Automated Deduction and Natural Language Understanding. [Citation Graph (0, 0)][DBLP ] Conf ] Peter B. Andrews , Chad E. Brown Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Baumgartner , Christian G. Fermüller , Nicolas Peltier , Hantao Zhang Workshop: Model Computation - Principles, Algorithms, Applications. [Citation Graph (0, 0)][DBLP ] Conf ] Carsten Schürmann Workshop: Automation of Proofs by Mathematical Induction. [Citation Graph (0, 0)][DBLP ] Conf ] Didier Galmiche Workshop: Type-Theoretic Languages: Proof-Search and Semantics. [Citation Graph (0, 0)][DBLP ] Conf ] Erica Melis Workshop: Automated Deduction in Education. [Citation Graph (0, 0)][DBLP ] Conf ] Simon Colton , Volker Sorge , Ursula Martin Workshop: The Role of Automated Deduction in Mathematics. [Citation Graph (0, 0)][DBLP ] Conf ] 