Search results for "Tableaux"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
48	Marianna Girlando, Björn Lellmann, Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis	VINTE: An Implementation of Internal Calculi for Lewis' Logics of Counterfactual Reasoning.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Wolfgang Bibel	A Vision for Automated Deduction Rooted in the Connection Method.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Serenella Cerrito, Amélie David 0001	Minimisation of ATL ^* Models.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Ori Lahav 0001, Yoni Zohar	Cut-Admissibility as a Corollary of the Subformula Property.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Christian G. Fermüller, Timo Lang	Interpreting Sequent Calculi as Client-Server Games.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Katalin Bimbó	On the Decidability of Certain Semi-Lattice Based Modal Logics.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Reuben N. S. Rowe, James Brotherston	Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Hans de Nivelle (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Mauro Ferrari 0002, Camillo Fiorentini	Proof-Search in Natural Deduction Calculus for Classical Propositional Logic.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Christoph Benzmüller	Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Annemarie Borg, Roman Kuznets	Realization Theorems for Justification Logics: Full Modularity.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Renate A. Schmidt, Uwe Waldmann	Modal Tableau Systems with Blocking and Congruence Closure.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Zakaria Chihani, Tomer Libal, Giselle Reis	The Proof Certifier Checkers.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Nicola Olivetti, Gian Luca Pozzato	A Standard Internal Calculus for Lewis' Counterfactual Logics.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Björn Lellmann	Linear Nested Sequents, 2-Sequents and Hypersequents.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Cláudia Nalon, Ullrich Hustadt, Clare Dixon	A Modal-Layered Resolution Calculus for K.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Ullrich Hustadt, Paul Gainer, Clare Dixon, Cláudia Nalon, Lan Zhang 0001	Ordered Resolution for Coalition Logic.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Agata Ciabattoni, Elisa Freschi, Francesco A. Genco, Björn Lellmann	Mīmāṃsā Deontic Logic: Proof Theory and Applications.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Peter Backeman, Philipp Rümmer	Efficient Algorithms for Bounded Rigid E-unification.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Michael Sioutis, Jean-François Condotta, Yakoub Salhi, Bertrand Mazure	Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	John Christopher McCabe-Dansted, Mark Reynolds 0001	A Tableau for Bundled Strategies.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Alexander K. Hudek, David Toman 0001, Grant E. Weddell	On Enumerating Query Plans Using Analytic Tableau.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Roy Dyckhoff	Invited Talk: Coherentisation of First-Order Logic.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Taus Brock-Nannestad, Kaustuv Chaudhuri	Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	James Brotherston, Nikos Gorogiannis	Disproving Inductive Entailments in Separation Logic via Base Pair Approximation.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Christoph Wernhard	Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Sara Negri, Nicola Olivetti	A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Richard Bubel, Crystal Chang Din, Reiner Hähnle, Keiko Nakata 0001	A Dynamic Logic with Traces and Coinduction.	TABLEAUX	2015	DBLP DOI BibTeX RDF
48	Didier Galmiche, Dominique Larchey-Wendling (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Tobias Nipkow, Maximilian P. L. Haslbeck	A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Tim French 0002, John Christopher McCabe-Dansted, Mark Reynolds 0001	Model Checking General Linear Temporal Logic.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Nick Bezhanishvili, Silvio Ghilardi	Bounded Proofs and Step Frames.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Ulrich Furbach, Claudia Schon	Semantically Guided Evolution of ABoxes.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Ming Zuo, Volker Haarslev	Intelligent Tableau Algorithm for DL Reasoning.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Hidenori Kurokawa	Prefixed Tableau Systems for Logic of Proofs and Provability.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Amélie David 0001	TATL: Implementation of ATL Tableau-Based Decision Procedure.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Stéphane Graham-Lengrand	Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Björn Lellmann, Dirk Pattinson	Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Clark W. Barrett, Stéphane Demri, Morgan Deters	Witness Runs for Counter Machines - (Abstract).	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Davide Bresolin, Dario Della Monica, Angelo Montanari, Guido Sciavicco	A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky	A Refined Tableau Calculus with Controlled Blocking for the Description Logic.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Hendrik Tews	Formalizing Cut Elimination of Coalgebraic Logics in Coq.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Joseph Boudou, Bruno Woltzenlogel Paleo	Compression of Propositional Resolution Proofs by Lowering Subproofs.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Mauro Ferrari 0002, Camillo Fiorentini, Guido Fiorino	A Terminating Evaluation-Driven Variant of G3i.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Agata Ciabattoni, Paolo Maffezioli, Lara Spendier	Hypersequent and Labelled Calculi for Intermediate Logics.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Nicolas Peltier	Schemata of Formulæ in the Theory of Arrays.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Sara Negri	On the Duality of Proofs and Countermodels in Labelled Sequent Calculi.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Stefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia	Understanding Resolution Proofs through Herbrand's Theorem.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Christoph Röthlisberger	TAFA - A Tool for Admissibility in Finite Algebras.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Zhe Hou, Alwen Tiu, Rajeev Goré	A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search.	TABLEAUX	2013	DBLP DOI BibTeX RDF
48	Kai Brünnler, George Metcalfe (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Martin Lange	Tableaux(-like) Methods for the Satisfiability Problems of Temporal Logics.	TABLEAUX (Workshops, Tutorials, and Short Papers)	2011	DBLP BibTeX RDF
48	Dmitry Tishkovsky, Renate A. Schmidt, Mohammad Khodadadi	METTEL\textsc{Met\hspace{-.5pt}TeL}: A Tableau Prover with Logic-Independent Inference Engine.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Arnon Avron, Ori Lahav 0001	Kripke Semantics for Basic Sequent Systems.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Valerio Genovese, Laura Giordano 0001, Valentina Gliozzi, Gian Luca Pozzato	A Conditional Constructive Logic for Access Control and Its Sequent Calculus.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Vincent Aravantinos, Nicolas Peltier	Schemata of SMT-Problems.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Oliver Friedmann, Martin Lange	The Modal μ-Calculus Caught Off Guard.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Alwen Tiu	A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Laura Giordano 0001, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato	A Tableau Calculus for a Nonmonotonic Extension of EL^\mathcal{EL}^\bot.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	James Brotherston, Rajeev Goré	Craig Interpolation in Displayable Logics.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Maria Paola Bonacina, Moa Johansson	On Interpolation in Decision Procedures.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Davide Bresolin, Angelo Montanari, Pietro Sala, Guido Sciavicco	Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Agata Ciabattoni, Ori Lahav 0001, Anna Zamansky	Basic Constructive Connectives, Determinism and Matrix-Based Semantics.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Kazushige Terui	Proof Theory and Algebra in Substructural Logics.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Björn Lellmann, Dirk Pattinson	Cut Elimination for Shallow Modal Logics.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Anupam Das 0002	On the Proof Complexity of Cut-Free Bounded Deep Inference.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Régis Alenda, Nicola Olivetti	CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Mark Kaminski, Thomas Schneider 0002, Gert Smolka	Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Laura Bozzelli, Ruggero Lanotte	Hybrid and First-Order Complete Extensions of CaRet.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Jens Otten	A Non-clausal Connection Calculus.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Josef Urban, Jirí Vyskocil, Petr Stepánek	MaLeCoP Machine Learning Connection Prover.	TABLEAUX	2011	DBLP DOI BibTeX RDF
48	Martin Giese, Arild Waaler (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Natthapong Jungteerapanich	A Tableau System for the Modal µ-Calculus.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Peter Jeavons 0001	Presenting Constraints.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Silvio Ghilardi, Silvio Ranise	Goal-Directed Invariant Synthesis for Model Checking Modulo Theories.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Rajeev Goré, Linda Postniece, Alwen Tiu	Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Bianca Boretti, Sara Negri	Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Arnon Avron, Ori Lahav 0001	Canonical Constructive Systems.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Andrew Matusiewicz, Neil V. Murray, Erik Rosenthal	Prime Implicate Tries.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Rajeev Goré, Florian Widmann	Sound Global State Caching for ALC with Inverse Roles.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Marta Cialdea Mayer	Abduction and Consequence Generation in a Support System for the Design of Logical Multiple-Choice Questions.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Kai Brünnler, Lutz Straßburger	Modular Sequent Systems for Modal Logic.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Renate A. Schmidt, Dmitry Tishkovsky	Automated Synthesis of Tableau Calculi.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Luís Pinto 0001, Tarmo Uustalu	Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	George Metcalfe, Nicola Olivetti	Proof Systems for a Gödel Modal Logic.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Davide Bresolin, Angelo Montanari, Pietro Sala, Guido Sciavicco	A Tableau-Based System for Spatial Reasoning about Directional Relations.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Dirk Pattinson, Lutz Schröder	Generic Modal Cut Elimination Applied to Conditional Logics.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	David Baelde	On the Proof Theory of Regular Fixed Points.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Franz Baader, Andreas Bauer 0002, Peter Baumgartner 0001, Anne Cregan, Alfredo Gabaldon, Krystian Ji, Kevin Lee, David Rajaratnam, Rolf Schwitter	A Novel Architecture for Situation Awareness Systems.	TABLEAUX	2009	DBLP DOI BibTeX RDF
48	Nicola Olivetti (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Linda Buisman, Rajeev Goré	A Cut-Free Sequent Calculus for Bi-intuitionistic Logic.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	André Platzer	Differential Dynamic Logic for Verifying Parametric Hybrid Systems.	TABLEAUX	2007	DBLP DOI BibTeX RDF	verification of parametric hybrid systems, dynamic logic, quantifier elimination, sequent calculus
48	Piero A. Bonatti	Nonmonotonic Description Logics - Requirements, Theory, and Implementations.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Neil V. Murray, Erik Rosenthal	Updating Reduced Implicate Tries.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Davide Bresolin, Valentin Goranko, Angelo Montanari, Pietro Sala	Tableau Systems for Logics of Subinterval Structures over Dense Orderings.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Alessandro Avellone, Guido Fiorino, Ugo Moscato	Improvements to the Tableau Prover PITP.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Matthias Baaz, George Metcalfe	Proof Theory for First Order Lukasiewicz Logic.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Ekaterina Komendantskaya	A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	Philippe Balbiani, Hans P. van Ditmarsch, Andreas Herzig, Tiago de Lima	A Tableau Method for Public Announcement Logics.	TABLEAUX	2007	DBLP DOI BibTeX RDF
48	John-Jules Ch. Meyer	Our Quest for the Holy Grail of Agent Verification.	TABLEAUX	2007	DBLP DOI BibTeX RDF