Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link
27	Haruhiko Sato, Sarah Winkler	Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion.	CADE	2015	DBLP DOI BibTeX RDF
27	Peter Backeman, Philipp Rümmer	Theorem Proving with Bounded Rigid E-Unification.	CADE	2015	DBLP DOI BibTeX RDF
27	Jan Gorzny, Bruno Woltzenlogel Paleo	Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses.	CADE	2015	DBLP DOI BibTeX RDF
27	Giles Reger, Martin Suda 0001, Andrei Voronkov	Playing with AVATAR.	CADE	2015	DBLP DOI BibTeX RDF
27	Jesse Alama, Paul E. Oppenheimer, Edward N. Zalta	Automating Leibniz's Theory of Concepts.	CADE	2015	DBLP DOI BibTeX RDF
27	Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa	Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent.	CADE	2015	DBLP DOI BibTeX RDF
27	Kiraku Shintani, Nao Hirokawa	CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems.	CADE	2015	DBLP DOI BibTeX RDF
27	Cezary Kaliszyk, Stephan Schulz 0001, Josef Urban, Jirí Vyskocil	System Description: E.T. 0.1.	CADE	2015	DBLP DOI BibTeX RDF
27	Thomas Gransden, Neil Walkinshaw, Rajeev Raman	SEPIA: Search for Proofs Using Inferred Automata.	CADE	2015	DBLP DOI BibTeX RDF
27	Filip Maric, Predrag Janicic, Marko Malikovic	Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3.	CADE	2015	DBLP DOI BibTeX RDF
27	Andrew Reynolds 0001, Jasmin Christian Blanchette	A Decision Procedure for (Co)datatypes in SMT Solvers.	CADE	2015	DBLP DOI BibTeX RDF
27	Grant Olney Passmore	Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers.	CADE	2015	DBLP DOI BibTeX RDF
27	Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki 0001	MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers.	CADE	2015	DBLP DOI BibTeX RDF
27	Aleks Kissinger, Vladimir Zamdzhiev	Quantomatic: A Proof Assistant for Diagrammatic Reasoning.	CADE	2015	DBLP DOI BibTeX RDF
27	Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann	Termination Competition (termCOMP 2015).	CADE	2015	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Joshua Bax, Uwe Waldmann	Beagle - A Hierarchic Superposition Theorem Prover.	CADE	2015	DBLP DOI BibTeX RDF
27	Mnacho Echenim, Nicolas Peltier, Sophie Tourret	Quantifier-Free Equational Logic and Prime Implicate Generation.	CADE	2015	DBLP DOI BibTeX RDF
27	Lawrence C. Paulson	A Formalisation of Finite Automata Using Hereditarily Finite Sets.	CADE	2015	DBLP DOI BibTeX RDF
27	José Iborra, Naoki Nishida 0001, Germán Vidal, Akihisa Yamada 0002	Reducing Relative Termination to Dependency Pair Problems.	CADE	2015	DBLP DOI BibTeX RDF
27	Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen	A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited.	CADE	2015	DBLP DOI BibTeX RDF
27	André Platzer	A Uniform Substitution Calculus for Differential Dynamic Logic.	CADE	2015	DBLP DOI BibTeX RDF
27	Ashish Tiwari 0001, Adrià Gascón, Bruno Dutertre	Program Synthesis Using Dual Interpretation.	CADE	2015	DBLP DOI BibTeX RDF
27	Tomer Libal	Regular Patterns in Second-Order Unification.	CADE	2015	DBLP DOI BibTeX RDF
27	Maria Paola Bonacina (eds.)	Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings	CADE	2013	DBLP DOI BibTeX RDF
27	Nicolas Guenot	Nested Deduction in Logical Foundations for Computation. (Deduction Imbriquée et Fondements Logiques du Calcul).		2013	RDF
27	Cezary Kaliszyk, Josef Urban	PRocH: Proof Reconstruction for HOL Light.	CADE	2013	DBLP DOI BibTeX RDF
27	Marta Cialdea Mayer	A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies.	CADE	2013	DBLP DOI BibTeX RDF
27	Graeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte	Solving Difference Constraints over Modular Arithmetic.	CADE	2013	DBLP DOI BibTeX RDF
27	Richard Williams, Boris Konev	Propositional Temporal Proving with Reductions to a SAT Problem.	CADE	2013	DBLP DOI BibTeX RDF
27	Krystof Hoder, Andrei Voronkov	The 481 Ways to Split a Clause and Deal with Propositional Variables.	CADE	2013	DBLP DOI BibTeX RDF
27	Bernhard Beckert, Daniel Bruns	Dynamic Logic with Trace Semantics.	CADE	2013	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems.	CADE	2013	DBLP DOI BibTeX RDF
27	Zakaria Chihani, Dale Miller 0001, Fabien Renaud	Foundational Proof Certificates in First-Order Logic.	CADE	2013	DBLP DOI BibTeX RDF
27	Markus Bender, Björn Pelzer, Claudia Schon	System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description Logic.	CADE	2013	DBLP DOI BibTeX RDF
27	Franz Baader, Stefan Borgwardt, Marcel Lippmann	Temporalizing Ontology-Based Data Access.	CADE	2013	DBLP DOI BibTeX RDF
27	Mark Kaminski, Tobias Tebbi	InKreSAT: Modal Reasoning via Incremental Reduction to SAT.	CADE	2013	DBLP DOI BibTeX RDF
27	Radu Iosif, Adam Rogalewicz, Jirí Simácek	The Tree Width of Separation Logic with Recursive Definitions.	CADE	2013	DBLP DOI BibTeX RDF
27	Serdar Erbatur, Santiago Escobar 0001, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows 0001, José Meseguer 0001, Paliath Narendran, Sonia Santiago, Ralf Sasse	Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.	CADE	2013	DBLP DOI BibTeX RDF
27	Andrew Reynolds 0001, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett	Quantifier Instantiation Techniques for Finite Model Finding in SMT.	CADE	2013	DBLP DOI BibTeX RDF
27	Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo	Towards Modularly Comparing Programs Using Automated Theorem Provers.	CADE	2013	DBLP DOI BibTeX RDF
27	Noran Azmy, Christoph Weidenbach	Computing Tiny Clause Normal Forms.	CADE	2013	DBLP DOI BibTeX RDF
27	Bernhard Beckert, Rajeev Goré, Carsten Schürmann 0001	Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme.	CADE	2013	DBLP DOI BibTeX RDF
27	Daniel Kühlwein, Stephan Schulz 0001, Josef Urban	E-MaLeS 1.1.	CADE	2013	DBLP DOI BibTeX RDF
27	Jasmin Christian Blanchette, Andrei Paskevich	TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.	CADE	2013	DBLP DOI BibTeX RDF
27	Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri	Tractable Inference Systems: An Extension with a Deducibility Predicate.	CADE	2013	DBLP DOI BibTeX RDF
27	Jean-Christophe Filliâtre	One Logic to Use Them All.	CADE	2013	DBLP DOI BibTeX RDF
27	Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone	Automating Inductive Proofs Using Theory Exploration.	CADE	2013	DBLP DOI BibTeX RDF
27	Reiner Hähnle, Ina Schaefer, Richard Bubel	Reuse in Software Verification by Abstract Method Calls.	CADE	2013	DBLP DOI BibTeX RDF
27	Leonardo Mendonça de Moura, Grant Olney Passmore	Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.	CADE	2013	DBLP DOI BibTeX RDF
27	Natarajan Shankar	Automated Reasoning, Fast and Slow.	CADE	2013	DBLP DOI BibTeX RDF
27	Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler	Verifying Refutations with Extended Resolution.	CADE	2013	DBLP DOI BibTeX RDF
27	Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen	Hierarchical Combination.	CADE	2013	DBLP DOI BibTeX RDF
27	Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker 0001	A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition.	CADE	2013	DBLP DOI BibTeX RDF
27	Sicun Gao, Soonho Kong, Edmund M. Clarke	dReal: An SMT Solver for Nonlinear Theories over the Reals.	CADE	2013	DBLP DOI BibTeX RDF
27	Rajeev Goré, Jimmy Thomson 0001	An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description.	CADE	2013	DBLP DOI BibTeX RDF
27	Abdelkader Kersani, Nicolas Peltier	Completeness and Decidability Results for First-Order Clauses with Indices.	CADE	2013	DBLP DOI BibTeX RDF
27	Gergely Kovásznai, Andreas Fröhlich, Armin Biere	: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into.	CADE	2013	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Uwe Waldmann	Hierarchic Superposition with Weak Abstraction.	CADE	2013	DBLP DOI BibTeX RDF
27	Laurent Vigneron	Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis. (Automated Deduction applied to the Analysis and Verification of Infinite State Systems).		2011	RDF
27	Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans (eds.)	Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings	CADE	2011	DBLP DOI BibTeX RDF
27	Hicham Bensaid	Utilisation des schématisations de termes en déduction automatique. (Using term schematisations in automated deduction).		2011	RDF
27	Pavel Klinov, Bijan Parsia	A Hybrid Method for Probabilistic Satisfiability.	CADE	2011	DBLP DOI BibTeX RDF
27	Konstantin Korovin, Andrei Voronkov	Solving Systems of Linear Inequalities by Bound Propagation.	CADE	2011	DBLP DOI BibTeX RDF
27	Koen Claessen	The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract).	CADE	2011	DBLP DOI BibTeX RDF
27	Matthew Fredrikson, Mihai Christodorescu, Somesh Jha	Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms.	CADE	2011	DBLP DOI BibTeX RDF
27	Aarne Ranta	Translating between Language and Logic: What Is Easy and What Is Difficult.	CADE	2011	DBLP DOI BibTeX RDF
27	Chad E. Brown	Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems.	CADE	2011	DBLP DOI BibTeX RDF
27	Matthias Horbach	System Description: SPASS-FD.	CADE	2011	DBLP DOI BibTeX RDF
27	Koen Claessen, Ann Lillieström, Nicholas Smallbone	Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic.	CADE	2011	DBLP DOI BibTeX RDF
27	Armin Biere, Florian Lonsing, Martina Seidl	Blocked Clause Elimination for QBF.	CADE	2011	DBLP DOI BibTeX RDF
27	Zhiqiang Liu, Christopher Lynch	Efficient General Unification for XOR with Homomorphism.	CADE	2011	DBLP DOI BibTeX RDF
27	Ali Sinan Köksal, Viktor Kuncak, Philippe Suter	Scala to the Power of Z3: Integrating SMT and Programming.	CADE	2011	DBLP DOI BibTeX RDF
27	Étienne Payet, Fausto Spoto	Static Analysis of Android Programs.	CADE	2011	DBLP DOI BibTeX RDF
27	James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen	Automated Cyclic Entailment Proofs in Separation Logic.	CADE	2011	DBLP DOI BibTeX RDF
27	André Platzer	Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.	CADE	2011	DBLP DOI BibTeX RDF
27	Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune	Deciding Security for Protocols with Recursive Tests.	CADE	2011	DBLP DOI BibTeX RDF
27	Byron Cook	Advances in Proving Program Termination and Liveness.	CADE	2011	DBLP DOI BibTeX RDF
27	Matthias Horbach	Predicate Completion for non-Horn Clause Sets.	CADE	2011	DBLP DOI BibTeX RDF
27	Sarah Winkler, Aart Middeldorp	AC Completion with Termination Tools.	CADE	2011	DBLP DOI BibTeX RDF
27	Didier Galmiche, Daniel Méry	A Connection-Based Characterization of Bi-intuitionistic Validity.	CADE	2011	DBLP DOI BibTeX RDF
27	Laura Kovács, Georg Moser, Andrei Voronkov	On Transfinite Knuth-Bendix Orders.	CADE	2011	DBLP DOI BibTeX RDF
27	Thomas Wies, Marco Muñiz, Viktor Kuncak	An Efficient Decision Procedure for Imperative Tree Data Structures.	CADE	2011	DBLP DOI BibTeX RDF
27	Krystof Hoder, Andrei Voronkov	Sine Qua Non for Large Theory Reasoning.	CADE	2011	DBLP DOI BibTeX RDF
27	Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson	Extending Sledgehammer with SMT Solvers.	CADE	2011	DBLP DOI BibTeX RDF
27	Volker Haarslev, Roberto Sebastiani, Michele Vescovi	Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT.	CADE	2011	DBLP DOI BibTeX RDF
27	Sascha Böhme, Michal Moskal	Heaps and Data Structures: A Challenge for Automated Provers.	CADE	2011	DBLP DOI BibTeX RDF
27	Francesco Alberti, Alessandro Armando, Silvio Ranise	ASASP: Automated Symbolic Analysis of Security Policies.	CADE	2011	DBLP DOI BibTeX RDF
27	Michael Schneider 0001, Geoff Sutcliffe	Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving.	CADE	2011	DBLP DOI BibTeX RDF
27	Alexandros Chortaras, Despoina Trivela, Giorgos B. Stamou	Optimized Query Rewriting for OWL 2 QL.	CADE	2011	DBLP DOI BibTeX RDF
27	Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo	Compression of Propositional Resolution Proofs via Partial Regularization.	CADE	2011	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001, Cesare Tinelli	Model Evolution with Equality Modulo Built-in Theories.	CADE	2011	DBLP DOI BibTeX RDF
27	David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo	Exploiting Symmetry in SMT Problems.	CADE	2011	DBLP DOI BibTeX RDF
27	Dejan Jovanovic, Leonardo Mendonça de Moura	Cutting to the Chase Solving Linear Integer Arithmetic.	CADE	2011	DBLP DOI BibTeX RDF
27	Harald Zankl, Bertram Felgenhauer, Aart Middeldorp	CSI - A Confluence Tool.	CADE	2011	DBLP DOI BibTeX RDF
27	Lars Noschinski, Fabian Emmes, Jürgen Giesl	A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems.	CADE	2011	DBLP DOI BibTeX RDF
27	María Alpuente, Demis Ballis, Javier Espert, Daniel Romero 0001	Backward Trace Slicing for Rewriting Logic Theories.	CADE	2011	DBLP DOI BibTeX RDF
27	Franz Baader, Thanh Binh Nguyen 0003, Stefan Borgwardt, Barbara Morawska 0001	Unification in the Description Logic EL without the Top Concept.	CADE	2011	DBLP DOI BibTeX RDF
27	Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi	The Matita Interactive Theorem Prover.	CADE	2011	DBLP DOI BibTeX RDF
27	Daniele Nantes Sobrinho, Mauricio Ayala-Rincón	Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures.	WoLLIC	2010	DBLP DOI BibTeX RDF
27	Renate A. Schmidt (eds.)	Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings	CADE	2009	DBLP DOI BibTeX RDF