Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link
27	Fajar Haifani, Sophie Tourret, Christoph Weidenbach	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance.	CADE	2021	DBLP DOI BibTeX RDF
27	Christoph Wernhard, Wolfgang Bibel	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures.	CADE	2021	DBLP DOI BibTeX RDF
27	Dohan Kim 0001, Christopher Lynch	Equational Theorem Proving Modulo.	CADE	2021	DBLP DOI BibTeX RDF
27	Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic	Superposition with First-class Booleans and Inprocessing Clausification.	CADE	2021	DBLP DOI BibTeX RDF
27	Akihisa Yamada 0002	Multi-Dimensional Interpretations for Termination of Term Rewriting.	CADE	2021	DBLP DOI BibTeX RDF
27	Pascal Fontaine (eds.)	Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings	CADE	2019	DBLP DOI BibTeX RDF
27	André Platzer	Uniform Substitution at One Fell Swoop.	CADE	2019	DBLP DOI BibTeX RDF
27	Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar	Automata Terms in a Lazy WSkS Decision Procedure.	CADE	2019	DBLP DOI BibTeX RDF
27	Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch	Unification Modulo Lists with Reverse Relation with Certain Word Equations.	CADE	2019	DBLP DOI BibTeX RDF
27	Katherine Cordwell, André Platzer	Towards Physical Hybrid Systems.	CADE	2019	DBLP DOI BibTeX RDF
27	Christina Kohl, Aart Middeldorp	Composing Proof Terms.	CADE	2019	DBLP DOI BibTeX RDF
27	Alexsander Andrade de Melo, Mateus de Oliveira Oliveira	On the Width of Regular Classes of Finite Structures.	CADE	2019	DBLP DOI BibTeX RDF
27	Christian Sternagel, Sarah Winkler	Certified Equational Reasoning via Ordered Completion.	CADE	2019	DBLP DOI BibTeX RDF
27	Michael Rawson 0001, Giles Reger	Old or Heavy? Decaying Gracefully with Age/Weight Shapes.	CADE	2019	DBLP DOI BibTeX RDF
27	Yizheng Zhao, Renate A. Schmidt	FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions.	CADE	2019	DBLP DOI BibTeX RDF
27	Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi	Confluence by Critical Pair Analysis Revisited.	CADE	2019	DBLP DOI BibTeX RDF
27	Stephan Schulz 0001, Simon Cruanes, Petar Vukmirovic	Faster, Higher, Stronger: E 2.3.	CADE	2019	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe, Francis Jeffry Pelletier	JGXYZ: An ATP System for Gap and Glut Logics.	CADE	2019	DBLP DOI BibTeX RDF
27	Ulrich Furbach, Teresa Krämer, Claudia Schon	Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection.	CADE	2019	DBLP DOI BibTeX RDF
27	Jürgen Giesl, Peter Giesl, Marcel Hark	Computing Expected Runtimes for Constant Probability Programs.	CADE	2019	DBLP DOI BibTeX RDF
27	Giles Reger, Andrei Voronkov	Induction in Saturation-Based Proof Search.	CADE	2019	DBLP DOI BibTeX RDF
27	David A. Plaisted	The Aspect Calculus.	CADE	2019	DBLP DOI BibTeX RDF
27	Raúl Gutiérrez, Salvador Lucas	Automatic Generation of Logical Models with AGES.	CADE	2019	DBLP DOI BibTeX RDF
27	Valentin Cassano, Raul Fervari, Guillaume Hoffmann 0001, Carlos Areces, Pablo F. Castro	A Tableaux Calculus for Default Intuitionistic Logic.	CADE	2019	DBLP DOI BibTeX RDF
27	Haniel Barbosa, Andrew Reynolds 0001, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett	Extending SMT Solvers to Higher-Order Logic.	CADE	2019	DBLP DOI BibTeX RDF
27	Andrei Popescu 0001, Dmitriy Traytel	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.	CADE	2019	DBLP DOI BibTeX RDF
27	Dennis Peuter, Viorica Sofronie-Stokkermans	On Invariant Synthesis for Parametric Systems.	CADE	2019	DBLP DOI BibTeX RDF
27	Di Long Li, Alwen Tiu	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification.	CADE	2019	DBLP DOI BibTeX RDF
27	Patrick Trentin, Roberto Sebastiani	Optimization Modulo the Theory of Floating-Point Numbers.	CADE	2019	DBLP DOI BibTeX RDF
27	Tanel Tammet	GKC: A Reasoning System for Large Knowledge Bases.	CADE	2019	DBLP DOI BibTeX RDF
27	Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban	GRUNGE: A Grand Unified ATP Challenge.	CADE	2019	DBLP DOI BibTeX RDF
27	Karel Chvalovský, Jan Jakubuv, Martin Suda 0001, Josef Urban	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.	CADE	2019	DBLP DOI BibTeX RDF
27	Mingshuai Chen, Jian Wang 0042, Jie An 0001, Bohua Zhan, Deepak Kapur, Naijun Zhan	NIL: Learning Nonlinear Interpolants.	CADE	2019	DBLP DOI BibTeX RDF
27	Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin	Model Completeness, Covers and Superposition.	CADE	2019	DBLP DOI BibTeX RDF
27	Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach	SPASS-SATT - A CDCL(LA) Solver.	CADE	2019	DBLP DOI BibTeX RDF
27	Rose Bohrer, Manuel Fernández 0005, André Platzer	dLι: Definite Descriptions in Differential Dynamic Logic.	CADE	2019	DBLP DOI BibTeX RDF
27	Alberto Fiori, Christoph Weidenbach	SCL Clause Learning from Simple Models.	CADE	2019	DBLP DOI BibTeX RDF
27	Aina Niemetz, Mathias Preiner, Andrew Reynolds 0001, Yoni Zohar, Clark W. Barrett, Cesare Tinelli	Towards Bit-Width-Independent Proofs in SMT Solvers.	CADE	2019	DBLP DOI BibTeX RDF
27	Ahmed Bhayat, Giles Reger	Restricted Combinatory Unification.	CADE	2019	DBLP DOI BibTeX RDF
27	Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann	Superposition with Lambdas.	CADE	2019	DBLP DOI BibTeX RDF
27	Arnold Beckmann, Norbert Preining	Hyper Natural Deduction for Gödel Logic - A natural deduction system for parallel reasoning.	J. Log. Comput.	2018	DBLP DOI BibTeX RDF
27	Declan Thompson, Jeremy Seligman	Teaching Natural Deduction in the Right Order with Natural Deduction Planner.	FLAP	2017	DBLP BibTeX RDF
27	Leonardo de Moura 0001 (eds.)	Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings	CADE	2017	DBLP DOI BibTeX RDF
27	Delia Kesner, Pierre Vial	Types as Resources for Classical Natural Deduction.	FSCD	2017	DBLP DOI BibTeX RDF
27	Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand	A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms.	CADE	2017	DBLP DOI BibTeX RDF
27	Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar	Satisfiability Modulo Theories and Assignments.	CADE	2017	DBLP DOI BibTeX RDF
27	Baoluo Meng, Andrew Reynolds 0001, Cesare Tinelli, Clark W. Barrett	Relational Constraint Solving in SMT.	CADE	2017	DBLP DOI BibTeX RDF
27	Benjamin Kiesl, Martin Suda 0001	A Unifying Principle for Clause Elimination in First-Order Logic.	CADE	2017	DBLP DOI BibTeX RDF
27	Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani	Satisfiability Modulo Transcendental Functions via Incremental Linearization.	CADE	2017	DBLP DOI BibTeX RDF
27	Markus Bender, Viorica Sofronie-Stokkermans	Decision Procedures for Theories of Sets with Measures.	CADE	2017	DBLP DOI BibTeX RDF
27	Simon Cruanes	Satisfiability Modulo Bounded Checking.	CADE	2017	DBLP DOI BibTeX RDF
27	Mnacho Echenim, Nicolas Peltier	The Binomial Pricing Model in Finance: A Formalization in Isabelle.	CADE	2017	DBLP DOI BibTeX RDF
27	Zhaowei Xu, Taolue Chen, Zhilin Wu	Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints.	CADE	2017	DBLP DOI BibTeX RDF
27	Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine	Scalable Fine-Grained Proofs for Formula Processing.	CADE	2017	DBLP DOI BibTeX RDF
27	Matthias Horbach, Marco Voigt, Christoph Weidenbach	On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic.	CADE	2017	DBLP DOI BibTeX RDF
27	Stephan Schulz 0001, Geoff Sutcliffe, Josef Urban, Adam Pease	Detecting Inconsistencies in Large First-Order Knowledge Bases.	CADE	2017	DBLP DOI BibTeX RDF
27	José Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene	Towards Logic-Based Verification of JavaScript Programs.	CADE	2017	DBLP DOI BibTeX RDF
27	Ullrich Hustadt, Ana Ozaki, Clare Dixon	Theorem Proving for Metric Temporal Logic over the Naturals.	CADE	2017	DBLP DOI BibTeX RDF
27	James Brotherston, Nikos Gorogiannis, Max I. Kanovich	Biabduction (and Related Problems) in Array Separation Logic.	CADE	2017	DBLP DOI BibTeX RDF
27	Yutaka Nagashima, Ramana Kumar	A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.	CADE	2017	DBLP DOI BibTeX RDF
27	Florian Lonsing, Uwe Egly	DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL.	CADE	2017	DBLP DOI BibTeX RDF
27	Petros Papapanagiotou, Jacques D. Fleuriot	WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition.	CADE	2017	DBLP DOI BibTeX RDF
27	Marijn J. H. Heule, Benjamin Kiesl, Armin Biere	Short Proofs Without New Variables.	CADE	2017	DBLP DOI BibTeX RDF
27	Maximiliano Cristiá, Gianfranco Rossi	A Decision Procedure for Restricted Intensional Sets.	CADE	2017	DBLP DOI BibTeX RDF
27	Gadi Tellez, James Brotherston	Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof.	CADE	2017	DBLP DOI BibTeX RDF
27	Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp	Efficient Certified RAT Verification.	CADE	2017	DBLP DOI BibTeX RDF
27	Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen	Notions of Knowledge in Combinations of Theories Sharing Constructors.	CADE	2017	DBLP DOI BibTeX RDF
27	Andreas Teucke, Christoph Weidenbach	Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints.	CADE	2017	DBLP DOI BibTeX RDF
27	Julian Nagele, Bertram Felgenhauer, Aart Middeldorp	CSI: New Evidence - A Progress Report.	CADE	2017	DBLP DOI BibTeX RDF
27	June Andronick	Reasoning About Concurrency in High-Assurance, High-Performance Software Systems.	CADE	2017	DBLP DOI BibTeX RDF
27	Bernhard Gleiss, Laura Kovács, Martin Suda 0001	Splitting Proofs for Interpolation.	CADE	2017	DBLP DOI BibTeX RDF
27	Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo	Scavenger 0.1: A Theorem Prover Based on Conflict Resolution.	CADE	2017	DBLP DOI BibTeX RDF
27	Christian Sternagel, Thomas Sternagel	Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems.	CADE	2017	DBLP DOI BibTeX RDF
27	Grant Olney Passmore, Denis Ignatovich	Formal Verification of Financial Algorithms.	CADE	2017	DBLP DOI BibTeX RDF
27	Roberto Blanco, Zakaria Chihani, Dale Miller 0001	Translating Between Implicit and Explicit Versions of Proof.	CADE	2017	DBLP DOI BibTeX RDF
27	Michael Färber 0002, Cezary Kaliszyk, Josef Urban	Monte Carlo Tableau Proof Search.	CADE	2017	DBLP DOI BibTeX RDF
27	Peter Lammich	Efficient Verified (UN)SAT Certificate Checking.	CADE	2017	DBLP DOI BibTeX RDF
27	Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002	Certifying Safety and Termination Proofs for Integer Transition Systems.	CADE	2017	DBLP DOI BibTeX RDF
27	Pierre Halmagrand	Automated Deduction and Proof Certification for the B Method. (Déduction Automatique et Certification de Preuve pour la Méthode B).		2016	RDF
27	Gérard P. Huet	Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization.	FSCD	2016	DBLP DOI BibTeX RDF
27	Jeremy Seligman, Declan Thompson	Teaching natural deduction in the right order with Natural Deduction Planner.	CoRR	2015	DBLP BibTeX RDF
27	Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo.	LPAR (short papers)	2015	DBLP DOI BibTeX RDF
27	Amy P. Felty, Aart Middeldorp (eds.)	Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings	CADE	2015	DBLP DOI BibTeX RDF
27	Aurélie Montarnal	Deduction of inter-organizational collaborative business processes within an enterprise social network. (Déduction de processus métier collaboratifs inter-organisationnels au sein d'un réseau social d'entreprises).		2015	RDF
27	Amélie David 0001	Deciding ATL*Satisfiability by Tableaux.	CADE	2015	DBLP DOI BibTeX RDF
27	Salman Saghafi, Ryan Danas, Daniel J. Dougherty	Exploring Theories with a Model-Finding Assistant.	CADE	2015	DBLP DOI BibTeX RDF
27	Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler	Expressing Symmetry Breaking in DRAT Proofs.	CADE	2015	DBLP DOI BibTeX RDF
27	Takahito Aoto 0001, Nao Hirokawa, Julian Nagele, Naoki Nishida 0001, Harald Zankl	Confluence Competition 2015.	CADE	2015	DBLP DOI BibTeX RDF
27	Zhe Hou, Rajeev Goré, Alwen Tiu	Automated Theorem Proving for Assertions in Separation Logic with All Connectives.	CADE	2015	DBLP DOI BibTeX RDF
27	Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer	The Lean Theorem Prover (System Description).	CADE	2015	DBLP DOI BibTeX RDF
27	Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai	Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies.	CADE	2015	DBLP DOI BibTeX RDF
27	Martin Bromberger, Thomas Sturm 0001, Christoph Weidenbach	Linear Integer Arithmetic Revisited.	CADE	2015	DBLP DOI BibTeX RDF
27	Ulrich Furbach, Björn Pelzer, Claudia Schon	Automated Reasoning in the Wild.	CADE	2015	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001	SMTtoTPTP - A Converter for Theorem Proving Formats.	CADE	2015	DBLP DOI BibTeX RDF
27	Brigitte Pientka, Andrew Cave	Inductive Beluga: Programming Proofs.	CADE	2015	DBLP DOI BibTeX RDF
27	Crystal Chang Din, Richard Bubel, Reiner Hähnle	KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.	CADE	2015	DBLP DOI BibTeX RDF
27	Giles Reger, Dmitry Tishkovsky, Andrei Voronkov	Cooperating Proof Attempts.	CADE	2015	DBLP DOI BibTeX RDF
27	Philippe Balbiani, Joseph Boudou	Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition.	CADE	2015	DBLP DOI BibTeX RDF
27	Ursula Martin	Stumbling Around in the Dark: Lessons from Everyday Mathematics.	CADE	2015	DBLP DOI BibTeX RDF
27	Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer	KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems.	CADE	2015	DBLP DOI BibTeX RDF