Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Guillaume Burel	Bonnes démonstrations en déduction modulo. (Good proofs in deduction modulo).		2009	RDF
27	Shuvendu K. Lahiri, Shaz Qadeer	Complexity and Algorithms for Monomial and Clausal Predicate Abstraction.	CADE	2009	DBLP DOI BibTeX RDF
27	Mark E. Stickel	Building Theorem Provers.	CADE	2009	DBLP DOI BibTeX RDF
27	Amit Goel, Sava Krstic, Cesare Tinelli	Ground Interpolation for Combined Theories.	CADE	2009	DBLP DOI BibTeX RDF
27	Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch	Combinable Extensions of Abelian Groups.	CADE	2009	DBLP DOI BibTeX RDF
27	Alex Roederer, Yury Puzis, Geoff Sutcliffe	Divvy: An ATP Meta-system Based on Axiom Relevance Ordering.	CADE	2009	DBLP DOI BibTeX RDF
27	Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks	Complexity of Fractran and Productivity.	CADE	2009	DBLP DOI BibTeX RDF
27	Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp	Termination Analysis by Dependency Pairs and Inductive Theorem Proving.	CADE	2009	DBLP DOI BibTeX RDF
27	Feifei Ma, Sheng Liu, Jian Zhang 0001	Volume Computation for Boolean Combination of Linear Arithmetic Constraints.	CADE	2009	DBLP DOI BibTeX RDF
27	Koen Claessen, Ann Lillieström	Automated Inference of Finite Unsatisfiability.	CADE	2009	DBLP DOI BibTeX RDF
27	Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda 0001, Patrick Wischnewski	SPASS Version 3.5.	CADE	2009	DBLP DOI BibTeX RDF
27	Matthias Horbach, Christoph Weidenbach	Decidability Results for Saturation-Based Model Building.	CADE	2009	DBLP DOI BibTeX RDF
27	André Platzer, Jan-David Quesel, Philipp Rümmer	Real World Verification.	CADE	2009	DBLP DOI BibTeX RDF	hybrid systems, software verification, decision procedures, Real-closed fields
27	Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine	veriT: An Open, Trustable and Efficient SMT-Solver.	CADE	2009	DBLP DOI BibTeX RDF
27	Martin C. Rinard	Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival.	CADE	2009	DBLP DOI BibTeX RDF
27	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Interpolant Generation for UTVPI.	CADE	2009	DBLP DOI BibTeX RDF
27	Roberto Sebastiani, Michele Vescovi	Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis.	CADE	2009	DBLP DOI BibTeX RDF
27	Michel Ludwig, Ullrich Hustadt	Fair Derivations in Monodic Temporal Reasoning.	CADE	2009	DBLP DOI BibTeX RDF
27	Linh Anh Nguyen, Andrzej Szalas	A Tableau Calculus for Regular Grammar Logics with Converse.	CADE	2009	DBLP DOI BibTeX RDF
27	Konstantin Korovin	Instantiation-Based Automated Reasoning: From Theory to Practice.	CADE	2009	DBLP DOI BibTeX RDF
27	Stephan Falke 0001, Deepak Kapur	A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs.	CADE	2009	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss	Progress in the Development of Automated Theorem Proving for Higher-Order Logic.	CADE	2009	DBLP DOI BibTeX RDF
27	Martin Korp, Aart Middeldorp	Beyond Dependency Graphs.	CADE	2009	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Uwe Waldmann	Superposition and Model Evolution Combined.	CADE	2009	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	Locality Results for Certain Extensions of Theories with Bridging Functions.	CADE	2009	DBLP DOI BibTeX RDF
27	Rajeev Goré, Florian Widmann	An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability.	CADE	2009	DBLP DOI BibTeX RDF
27	Laura Kovács, Andrei Voronkov	Interpolation and Symbol Elimination.	CADE	2009	DBLP DOI BibTeX RDF
27	Stefan Ciobaca, Stéphanie Delaune, Steve Kremer	Computing Knowledge in Security Protocols under Convergent Equational Theories.	CADE	2009	DBLP DOI BibTeX RDF
27	Éric Grégoire, Bertrand Mazure, Cédric Piette	Does This Set of Clauses Overlap with at Least One MUS?	CADE	2009	DBLP DOI BibTeX RDF
27	Lan Zhang 0001, Ullrich Hustadt, Clare Dixon	A Refined Resolution Calculus for CTL.	CADE	2009	DBLP DOI BibTeX RDF
27	Sean McLaughlin, Frank Pfenning	Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method.	CADE	2009	DBLP DOI BibTeX RDF
27	Bernard Boigelot, Julien Brusten, Jérôme Leroux	A Generalization of Semenov's Theorem to Automata over Real Numbers.	CADE	2009	DBLP DOI BibTeX RDF
27	Hicham Bensaid, Ricardo Caferra, Nicolas Peltier	Dei: A Theorem Prover for Terms with Integer Exponents.	CADE	2009	DBLP DOI BibTeX RDF
27	Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio	Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic.	CADE	2009	DBLP DOI BibTeX RDF	polynomial constraints, SAT modulo theories, program analysis, termination, Constraint solving
27	Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura	On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving.	CADE	2009	DBLP DOI BibTeX RDF
27	Frank Pfenning (eds.)	Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings	CADE	2007	DBLP DOI BibTeX RDF
27	Guillem Godoy, Sophie Tison	On the Normalization and Unique Normalization Properties of Term Rewrite Systems.	CADE	2007	DBLP DOI BibTeX RDF
27	Björn Pelzer, Christoph Wernhard	System Description: E-KRHyper.	CADE	2007	DBLP DOI BibTeX RDF
27	Roger Antonsen, Arild Waaler	A Labelled System for IPL with Variable Splitting.	CADE	2007	DBLP DOI BibTeX RDF
27	Viktor Kuncak, Martin C. Rinard	Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic.	CADE	2007	DBLP DOI BibTeX RDF
27	Oleg Mürk, Daniel Larsson, Reiner Hähnle	KeY-C: A Tool for Verification of C Programs.	CADE	2007	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Ulrich Furbach, Björn Pelzer	Hyper Tableaux with Equality.	CADE	2007	DBLP DOI BibTeX RDF
27	Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp	Proving Termination by Bounded Increase.	CADE	2007	DBLP DOI BibTeX RDF
27	Christian Urban, Stefan Berghofer, Michael Norrish	Barendregt's Variable Convention in Rule Inductions.	CADE	2007	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001	Logical Engineering with Instance-Based Methods.	CADE	2007	DBLP DOI BibTeX RDF
27	Alexander Krauss 0001	Certified Size-Change Termination.	CADE	2007	DBLP DOI BibTeX RDF
27	John Harrison 0001	Automating Elementary Number-Theoretic Proofs Using Gröbner Bases.	CADE	2007	DBLP DOI BibTeX RDF
27	Osman Hasan, Sofiène Tahar	Formalization of Continuous Probability Distributions.	CADE	2007	DBLP DOI BibTeX RDF
27	Juan Antonio Navarro Pérez, Andrei Voronkov	Encodings of Bounded LTL Model Checking in Effectively Propositional Logic.	CADE	2007	DBLP DOI BibTeX RDF
27	Colin Stirling	Games, Automata and Matching.	CADE	2007	DBLP DOI BibTeX RDF
27	Gulay Ünel, David Toman 0001	An Incremental Technique for Automata-Based Decision Procedures.	CADE	2007	DBLP DOI BibTeX RDF
27	Boris Motik, Robert D. C. Shearer, Ian Horrocks 0001	Optimized Reasoning in Description Logics Using Hypertableaux.	CADE	2007	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe, Yury Puzis	SRASS - A Semantic Relevance Axiom Selection System.	CADE	2007	DBLP DOI BibTeX RDF
27	Maria Paola Bonacina, Mnacho Echenim	T-Decision by Decomposition.	CADE	2007	DBLP DOI BibTeX RDF
27	David Baelde, Andrew Gacek, Dale Miller 0001, Gopalan Nadathur, Alwen Tiu	The Bedwyr System for Model Checking over Syntactic Expressions.	CADE	2007	DBLP DOI BibTeX RDF
27	Samuli Heilala, Brigitte Pientka	Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4.	CADE	2007	DBLP DOI BibTeX RDF
27	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.	CADE	2007	DBLP DOI BibTeX RDF
27	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Efficient E-Matching for SMT Solvers.	CADE	2007	DBLP DOI BibTeX RDF
27	Guodong Li, Konrad Slind	Compilation as Rewriting in Higher Order Logic.	CADE	2007	DBLP DOI BibTeX RDF
27	Stephan Falke 0001, Deepak Kapur	Dependency Pairs for Rewriting with Non-free Constructors.	CADE	2007	DBLP DOI BibTeX RDF
27	Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic	System Description: SpassVersion 3.0.	CADE	2007	DBLP DOI BibTeX RDF
27	Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin 0005, Christopher Lynch, Ralph Eric McGregor	Encoding First Order Proofs in SAT.	CADE	2007	DBLP DOI BibTeX RDF
27	Yeting Ge, Clark W. Barrett, Cesare Tinelli	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.	CADE	2007	DBLP DOI BibTeX RDF
27	Adam Koprowski, Aart Middeldorp	Predictive Labeling with Dependency Pairs Using SAT.	CADE	2007	DBLP DOI BibTeX RDF
27	Markus Aderhold	Improvements in Formula Generalization.	CADE	2007	DBLP DOI BibTeX RDF
27	Christopher Lynch, Duc-Khanh Tran	Automatic Decidability and Combinability Revisited.	CADE	2007	DBLP DOI BibTeX RDF
27	Carsten Lutz, Frank Wolter	Conservative Extensions in the Lightweight Description Logic EL.	CADE	2007	DBLP DOI BibTeX RDF
27	K. Rustan M. Leino	Designing Verification Conditions for Software.	CADE	2007	DBLP DOI BibTeX RDF
27	Steven Eker, Narciso Martí-Oliet, José Meseguer 0001, Alberto Verdejo	Deduction, Strategies, and Rewriting.	STRATEGIES@IJCAR	2006	DBLP DOI BibTeX RDF
27	Robert Nieuwenhuis (eds.)	Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings	CADE	2005	DBLP DOI BibTeX RDF
27	Mnacho Echenim	Déduction et Unification dans les Théories Permutatives. (Deduction and Unification in Permutative Theories).		2005	RDF
27	Benjamin Wack	Typage et déduction dans le calcul de réécriture. (Type systems and deduction in the rewriting calculus).		2005	RDF
27	Claudio Castellini, Alan Smaill	Proof Planning for First-Order Temporal Logic.	CADE	2005	DBLP DOI BibTeX RDF
27	Alex Sinner, Thomas Kleemann	KRHyper - In Your Pocket.	CADE	2005	DBLP DOI BibTeX RDF
27	Guillaume Dufay, Amy P. Felty, Stan Matwin	Privacy-Sensitive Information Flow with JML.	CADE	2005	DBLP DOI BibTeX RDF
27	Marco Benedetti	sKizzo: A Suite to Evaluate and Certify QBFs.	CADE	2005	DBLP DOI BibTeX RDF
27	Franz Baader, Silvio Ghilardi	Connecting Many-Sorted Theories.	CADE	2005	DBLP DOI BibTeX RDF
27	Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick	On the Complexity of Equational Horn Clauses.	CADE	2005	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Cesare Tinelli	The Model Evolution Calculus with Equality.	CADE	2005	DBLP DOI BibTeX RDF
27	Sean Bechhofer, Ian Horrocks 0001, Daniele Turi	The OWL Instance Store: System Description.	CADE	2005	DBLP DOI BibTeX RDF
27	Jordi Levy, Joachim Niehren, Mateu Villaret	Well-Nested Context Unification.	CADE	2005	DBLP DOI BibTeX RDF
27	Christian Urban, Christine Tasson	Nominal Techniques in Isabelle/HOL.	CADE	2005	DBLP DOI BibTeX RDF	theorem-assistants, Lambda-calculus, nominal logic, structural induction
27	Evelyne Contejean, Pierre Corbineau	Reflecting Proofs in First-Order Logic with Equality.	CADE	2005	DBLP DOI BibTeX RDF
27	Sean McLaughlin, John Harrison 0001	A Proof-Producing Decision Procedure for Real Arithmetic.	CADE	2005	DBLP DOI BibTeX RDF
27	Mizuhito Ogawa, Eiichi Horita, Satoshi Ono	Proving Properties of Incremental Merkle Trees.	CADE	2005	DBLP DOI BibTeX RDF	temporal authentication, theorem prover, Merkle tree
27	Chad E. Brown	Reasoning in Extensional Type Theory with Equality.	CADE	2005	DBLP DOI BibTeX RDF
27	Ullrich Hustadt, Boris Konev, Renate A. Schmidt	Deciding Monodic Fragments by Temporal Resolution.	CADE	2005	DBLP DOI BibTeX RDF
27	Serge Autexier	The CoRe Calculus.	CADE	2005	DBLP DOI BibTeX RDF
27	Kaustuv Chaudhuri, Frank Pfenning	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.	CADE	2005	DBLP DOI BibTeX RDF
27	Tomasz Truderung	Regular Protocols and Attacks with Regular Knowledge.	CADE	2005	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	Hierarchic Reasoning in Local Theory Extensions.	CADE	2005	DBLP DOI BibTeX RDF
27	Greta Yorsh, Madanlal Musuvathi	A Combination Method for Generating Interpolants.	CADE	2005	DBLP DOI BibTeX RDF
27	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz 0001, Roberto Sebastiani	The MathSAT 3 System.	CADE	2005	DBLP DOI BibTeX RDF
27	Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava 0001, Greta Yorsh	Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures.	CADE	2005	DBLP DOI BibTeX RDF
27	Brigitte Pientka	Tabling for Higher-Order Logic Programming.	CADE	2005	DBLP DOI BibTeX RDF
27	Jian Zhang 0001	Computer Search for Counterexamples to Wilkie's Identity.	CADE	2005	DBLP DOI BibTeX RDF
27	Guillem Godoy, Ashish Tiwari 0001	Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules.	CADE	2005	DBLP DOI BibTeX RDF
27	Christian G. Fermüller, Reinhard Pichler	Model Representation via Contexts and Implicit Generalizations.	CADE	2005	DBLP DOI BibTeX RDF	Model computation, clause evaluation, model representation
27	Andreas Meier 0002, Erica Melis	System Description: Multi A Multi-strategy Proof Planner.	CADE	2005	DBLP DOI BibTeX RDF
27	Boris Konev, Frank Wolter, Michael Zakharyaschev	Temporal Logics over Transitive States.	CADE	2005	DBLP DOI BibTeX RDF