Search results for "deduction"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
31	Bruno Emond	Operations on Conceptual Structures and Pierce's System of Existential graphs.	ICCS	1993	DBLP DOI BibTeX RDF
31	Philippe le Chenadec	On Positive Occur-Checks in Unification.	MFCS	1988	DBLP DOI BibTeX RDF
29	Janusz Czelakowski, Don Pigozzi	Fregean logics with the multiterm deduction theorem and their algebraization.	Stud Logica	2004	DBLP DOI BibTeX RDF	equivalential logic, self-extensional logic, Leibniz congruence, deduction theorem, quasivariety, algebraizable logic, abstract algebraic logic, protoalgebraic logic
29	Luis M. Laita, Eugenio Roanes-Lozano, Luis de Ledesma, José-Antonio Alonso	A computer algebra approach to verification and deduction in many-valued knowledge systems.	Soft Comput.	1999	DBLP DOI BibTeX RDF	Automated deduction in many-valued logics, expert systems verification, computer algebra
29	Andrew Slater, Rajeev Goré, Joachim Posegga, Harald Vogt	cardTAP: Automated Deduction on a Smart Card.	Australian Joint Conference on Artificial Intelligence	1998	DBLP DOI BibTeX RDF	lean TAP, security, java, proof carrying code, automated deduction, tableaux
29	Gordon M. Crippen	Intervals and the deduction of drug binding site models.	HICSS (5)	1995	DBLP DOI BibTeX RDF	chemical structure, drug binding site models, binding affinities, common receptor macromolecule, receptor, energetic features, common binding site, chemical structures, pharmacophore, bioactive conformations, conformational flexibility, stereospecific binding, qualitative binding data, chemically similar ligands, biology computing, intervals, chemistry, deduction, geometric features, chemistry computing, computer algorithm, drugs
29	Daisuke Kimura, Yoshihiko Kakutani	Classical Natural Deduction for S4 Modal Logic.	APLAS	2009	DBLP DOI BibTeX RDF
29	Alexander Bolotov, Oleg M. Grigoriev 0001, Vasilyi Shangin	Natural Deduction Calculus for Computation Tree Logic.	John Vincent Atanasoff Symposium	2006	DBLP DOI BibTeX RDF
29	Alexander Bolotov, Artie Basukoski, Oleg M. Grigoriev 0001, Vasilyi Shangin	Natural Deduction Calculus for Linear-Time Temporal Logic.	JELIA	2006	DBLP DOI BibTeX RDF
29	Michael Leuschel, Germán Vidal	Forward Slicing by Conjunctive Partial Deduction and Argument Filtering.	ESOP	2005	DBLP DOI BibTeX RDF
29	Pascal Lafourcade 0001, Denis Lugiez, Ralf Treinen	Intruder Deduction for AC-Like Equational Theories with Homomorphisms.	RTA	2005	DBLP DOI BibTeX RDF
29	Peter Baumgartner 0001, Ulrich Furbach, Margret Groß-Hardt, Thomas Kleemann	Model Based Deduction for Database Schema Reasoning.	KI	2004	DBLP DOI BibTeX RDF
29	Richard Bonichon	TaMeD: A Tableau Method for Deduction Modulo.	IJCAR	2004	DBLP DOI BibTeX RDF
29	Frank M. Brown	Logistica 2.0: A Technology for Implementing Automatic Deduction Systems.	TABLEAUX	2003	DBLP DOI BibTeX RDF
29	José Oscar Olmedo-Aguirre, Guillermo Morales-Luna	Indeed : Interactive Deduction on Horn Clause Theories.	IBERAMIA	2002	DBLP DOI BibTeX RDF	Horn clause theories, interaction, Logic programming, automated theorem proving
29	Carsten Sinz, Jörg Denzinger, Jürgen Avenhaus, Wolfgang Küchlin	Combining Parallel and Distributed Search in Automated Equational Deduction.	PPAM	2001	DBLP DOI BibTeX RDF
29	Grigore Rosu	Complete Categorical Equational Deduction.	CSL	2001	DBLP DOI BibTeX RDF
29	Pierre E. Bonzon	An Abstract Machine for Classes of Communicating Agents Based on Deduction.	ATAL	2001	DBLP DOI BibTeX RDF
29	Helko Lehmann, Michael Leuschel	Solving Planning Problems by Partial Deduction.	LPAR	2000	DBLP DOI BibTeX RDF
29	Jonathan C. Martin, Michael Leuschel	Sonic Partial Deduction.	Ershov Memorial Conference	1999	DBLP DOI BibTeX RDF
29	Robert Glück, Michael Leuschel	Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification.	Ershov Memorial Conference	1999	DBLP DOI BibTeX RDF
29	Geert-Jan M. Kruijff	Robustness in Tabular Deduction for Multimodal Logical Grammar - Part 1.	TSD	1999	DBLP DOI BibTeX RDF
29	Grigori Mints	Normal deduction in the intuitionistic linear logic.	Arch. Math. Log.	1998	DBLP DOI BibTeX RDF	Mathematics Subject Classification (1991):F05, 03B45
29	François Bry, Sunna Torge 0001	A Deduction Method Complete for Refutation and Finite Satisfiability.	JELIA	1998	DBLP DOI BibTeX RDF
29	Furio Honsell, Marino Miculan	A Natural Deduction Approach to Dynamic Logic.	TYPES	1995	DBLP DOI BibTeX RDF
29	Jean Goubault, Joachim Posegga	BDDs and Automated Deduction.	ISMIS	1994	DBLP DOI BibTeX RDF
29	Robert Glück, Morten Heine Sørensen	Partial Deduction and Driving are Equivalent.	PLILP	1994	DBLP DOI BibTeX RDF
29	Alan M. Frisch, Richard B. Scherl	A Constraint Logic Approach to Modal Deduction.	JELIA	1990	DBLP DOI BibTeX RDF
29	Dieter Hutter	Guiding Induction Proofs.	CADE	1990	DBLP DOI BibTeX RDF
29	Rod M. Burstall, Furio Honsell	A Natural Deduction treatment of Operational Semantics.	FSTTCS	1988	DBLP DOI BibTeX RDF
29	David A. Schmidt	A Programming Notation for Tactical Reasoning.	CADE	1984	DBLP DOI BibTeX RDF
29	Stan Matwin, Tomasz Pietrzykowski	Exponential Improvement of Efficient Backtracking: data Structure and Implementation.	CADE	1982	DBLP DOI BibTeX RDF
27	Brigitte Pientka, Cesare Tinelli (eds.)	Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings	CADE	2023	DBLP DOI BibTeX RDF
27	Oliver Görlitz, Daniel Hausmann 0001, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description).	CADE	2023	DBLP DOI BibTeX RDF
27	Nikolaj S. Bjørner, Katalin Fazekas	On Incremental Pre-processing for SMT.	CADE	2023	DBLP DOI BibTeX RDF
27	Jonas Schöpf, Aart Middeldorp	Confluence Criteria for Logically Constrained Rewrite Systems.	CADE	2023	DBLP DOI BibTeX RDF
27	Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu	Iscalc: An Interactive Symbolic Computation Framework (System Description).	CADE	2023	DBLP DOI BibTeX RDF
27	Jan-Christoph Kassing, Jürgen Giesl	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs.	CADE	2023	DBLP DOI BibTeX RDF
27	Jera Hensel, Jürgen Giesl	Proving Termination of C Programs with Lists.	CADE	2023	DBLP DOI BibTeX RDF
27	Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson 0001	Superposition with Delayed Unification.	CADE	2023	DBLP DOI BibTeX RDF
27	Colin Rothgang, Florian Rabe 0001, Christoph Benzmüller	Theorem Proving in Dependently-Typed Higher-Order Logic.	CADE	2023	DBLP DOI BibTeX RDF
27	Gerald Whitters, Vivek Nigam, Carolyn L. Talcott	Incremental Rewriting Modulo SMT.	CADE	2023	DBLP DOI BibTeX RDF
27	Yu-Fang Chen 0001, Philipp Rümmer, Wei-Lun Tsai	A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification).	CADE	2023	DBLP DOI BibTeX RDF
27	Florian Bruse, Martin Lange, Sören Möller	Formal Reasoning About Influence in Natural Sciences Experiments.	CADE	2023	DBLP DOI BibTeX RDF
27	Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment.	CADE	2023	DBLP DOI BibTeX RDF
27	Manfred Schmidt-Schauß, Daniele Nantes-Sobrinho	Towards Fast Nominal Anti-unification of Letrec-Expressions.	CADE	2023	DBLP DOI BibTeX RDF
27	Andrzej Indrzejczak, Yaroslav I. Petrukhin	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus.	CADE	2023	DBLP DOI BibTeX RDF
27	Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic.	CADE	2023	DBLP DOI BibTeX RDF
27	Tanel Tammet, Priit Järv, Martin Verrev, Dirk Draheim	An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper).	CADE	2023	DBLP DOI BibTeX RDF
27	Florian Frohn, Jürgen Giesl	Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper).	CADE	2023	DBLP DOI BibTeX RDF
27	Jasmin Blanchette, Qi Qiu, Sophie Tourret	Verified Given Clause Procedures.	CADE	2023	DBLP DOI BibTeX RDF
27	Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov	Program Synthesis in Saturation.	CADE	2023	DBLP DOI BibTeX RDF
27	Lukas Stevens	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory.	CADE	2023	DBLP DOI BibTeX RDF
27	Tomás Fiedor, Lukás Holík, Martin Hruska, Adam Rogalewicz, Juraj Síc, Pavol Vargovcík	Reasoning About Regular Properties: A Comparative Study.	CADE	2023	DBLP DOI BibTeX RDF
27	Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler	Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT.	CADE	2023	DBLP DOI BibTeX RDF
27	Martin Bromberger, Chaahat Jain, Christoph Weidenbach	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning.	CADE	2023	DBLP DOI BibTeX RDF
27	Martin Bromberger, Martin Desharnais, Christoph Weidenbach	An Isabelle/HOL Formalization of the SCL(FOL) Calculus.	CADE	2023	DBLP DOI BibTeX RDF
27	Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.	CADE	2023	DBLP DOI BibTeX RDF
27	Robin Coutelier, Laura Kovács, Michael Rawson 0001, Jakob Rath	SAT-Based Subsumption Resolution.	CADE	2023	DBLP DOI BibTeX RDF
27	Marvin Brieger, Stefan Mitsch, André Platzer	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs.	CADE	2023	DBLP DOI BibTeX RDF
27	Katharina Kreuzer, Tobias Nipkow	Verification of NP-Hardness Reduction Functions for Exact Lattice Problems.	CADE	2023	DBLP DOI BibTeX RDF
27	Jeremias Berg, Bart Bogaerts 0001, Jakob Nordström, Andy Oertel, Dieter Vandesande	Certified Core-Guided MaxSAT Solving.	CADE	2023	DBLP DOI BibTeX RDF
27	Dennis Peuter, Viorica Sofronie-Stokkermans, Sebastian Thunert	On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics Eℒ, Eℒ+.	CADE	2023	DBLP DOI BibTeX RDF
27	Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp	Left-Linear Completion with AC Axioms.	CADE	2023	DBLP DOI BibTeX RDF
27	Bernard Boigelot, Pascal Fontaine, Baptiste Vergain	Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates.	CADE	2023	DBLP DOI BibTeX RDF
27	Mathias Fleury, Peter Lammich	A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper).	CADE	2023	DBLP DOI BibTeX RDF
27	André Platzer, Geoff Sutcliffe (eds.)	Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings	CADE	2021	DBLP DOI BibTeX RDF
27	Didier Galmiche, Marta Gawek, Daniel Méry	Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity.	FSCD	2021	DBLP DOI BibTeX RDF
27	Tanel Tammet, Dirk Draheim, Priit Järv	Confidences for Commonsense Reasoning.	CADE	2021	DBLP DOI BibTeX RDF
27	Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais	Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.	CADE	2021	DBLP DOI BibTeX RDF
27	Joanna Golinska-Pilarek, Taneli Huuskonen, Michal Zawidzki	Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity.	CADE	2021	DBLP DOI BibTeX RDF
27	Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova	Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures.	CADE	2021	DBLP DOI BibTeX RDF
27	Emre Yolcu, Scott Aaronson, Marijn J. H. Heule	An Automated Approach to the Collatz Conjecture.	CADE	2021	DBLP DOI BibTeX RDF
27	Ying Sheng 0007, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli	Politeness and Stable Infiniteness: Stronger Together.	CADE	2021	DBLP DOI BibTeX RDF
27	Filip Bártek, Martin Suda 0001	Neural Precedence Recommender.	CADE	2021	DBLP DOI BibTeX RDF
27	Vivek Nigam, Giselle Reis, Samar Rahmouni, Harald Ruess	Proof Search and Certificates for Evidential Transactions.	CADE	2021	DBLP DOI BibTeX RDF
27	Jacob Errington, Junyoung Jang 0001, Brigitte Pientka	Harpoon: Mechanizing Metatheory Interactively - (System Description).	CADE	2021	DBLP DOI BibTeX RDF
27	Ryan Krueger, Jesse Michael Han, Daniel Selsam	Automatically Building Diagrams for Olympiad Geometry Problems.	CADE	2021	DBLP DOI BibTeX RDF
27	Markus N. Rabe, Christian Szegedy	Towards the Automatic Mathematician.	CADE	2021	DBLP DOI BibTeX RDF
27	Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller	The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints.	CADE	2021	DBLP DOI BibTeX RDF
27	Camillo Fiorentini	Efficient SAT-based Proof Search in Intuitionistic Propositional Logic.	CADE	2021	DBLP DOI BibTeX RDF
27	Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon	Efficient Local Reductions to Basic Modal Logic.	CADE	2021	DBLP DOI BibTeX RDF
27	Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel	The Isabelle/Naproche Natural Language Proof Assistant.	CADE	2021	DBLP DOI BibTeX RDF
27	Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret	Making Higher-Order Superposition Work.	CADE	2021	DBLP DOI BibTeX RDF
27	Emery A. Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori	A Normative Supervisor for Reinforcement Learning Agents.	CADE	2021	DBLP DOI BibTeX RDF
27	Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic	Superposition for Full Higher-order Logic.	CADE	2021	DBLP DOI BibTeX RDF
27	Kaustuv Chaudhuri	Subformula Linking for Intuitionistic Logic with Application to Type Theory.	CADE	2021	DBLP DOI BibTeX RDF
27	Alessandro Cimatti, Alberto Griggio, Gianluca Redondi	Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning.	CADE	2021	DBLP DOI BibTeX RDF
27	Leonardo de Moura 0001, Sebastian Ullrich 0002	The Lean 4 Theorem Prover and Programming Language.	CADE	2021	DBLP DOI BibTeX RDF
27	Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes.	CADE	2021	DBLP DOI BibTeX RDF
27	Mnacho Echenim, Radu Iosif, Nicolas Peltier	Unifying Decidable Entailments in Separation Logic with Inductive Definitions.	CADE	2021	DBLP DOI BibTeX RDF
27	Martin Suda 0001	Improving ENIGMA-style Clause Selection while Learning From History.	CADE	2021	DBLP DOI BibTeX RDF
27	Randal E. Bryant, Marijn J. H. Heule	Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver.	CADE	2021	DBLP DOI BibTeX RDF
27	Runqing Xu, Liming Li, Bohua Zhan	Verified Interactive Computation of Definite Integrals.	CADE	2021	DBLP DOI BibTeX RDF
27	Tobias Nipkow, Simon Roßkopf	Isabelle's Metalogic: Formalization and Proof Checker.	CADE	2021	DBLP DOI BibTeX RDF
27	Nicholas Smallbone	Twee: An Equational Theorem Prover.	CADE	2021	DBLP DOI BibTeX RDF
27	Lee A. Barnett, Armin Biere	Non-clausal Redundancy Properties.	CADE	2021	DBLP DOI BibTeX RDF
27	Petra Hozzová, Laura Kovács, Andrei Voronkov	Integer Induction in Saturation.	CADE	2021	DBLP DOI BibTeX RDF
27	Gabriel Ebner, Jasmin Blanchette, Sophie Tourret	A Unifying Splitting Framework.	CADE	2021	DBLP DOI BibTeX RDF
27	Peter Baumgartner 0001	The Fusemate Logic Programming System.	CADE	2021	DBLP DOI BibTeX RDF