Search results for "Tableaux"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
55	Norbert E. Fuchs, Uta Schwertel, Sunna Torge 0001	Controlled Natural Language Can Replace First-Order Logic.	ASE	1999	DBLP DOI BibTeX RDF	Attempto Controlled English, EP Tableaux, database schema design, Schubert's Steamroller, formal methods, model generation, controlled natural language, automatic reasoning
51	Leopoldo E. Bertossi, Camilla Schwind	Analytic Tableaux and Database Repairs: Foundations.	FoIKS	2002	DBLP DOI BibTeX RDF
51	Giuseppe De Giacomo, Fabio Massacci	Tableaux and Algorithms for Propositional Dynamic Logic with Converse.	CADE	1996	DBLP DOI BibTeX RDF
51	Fabio Massacci	Strongly Analytic Tableaux for Normal Modal Logics.	CADE	1994	DBLP DOI BibTeX RDF
51	Joanna Golinska-Pilarek, Ewa Orlowska	Tableaux and Dual Tableaux: Transformation of Proofs.	Stud Logica	2007	DBLP DOI BibTeX RDF	first-order logic with identity, tableaux systems, Rasiowa-Sikorski proof system
48	Slim Abdennadher, Heribert Schütz	Model Generation with Existentially Quantified Variables and Constraints.	ALP/HOA	1997	DBLP DOI BibTeX RDF
48	Jens Otten, Wolfgang Bibel (eds.)	Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) affiliated with the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), Prague, Czech Republic, September 18, 2023.	AReCCa@TABLEAUX	2024	DBLP BibTeX RDF
48	Revantha Ramanayake, Josef Urban (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Ineke van der Berg, Andrea De Domenico, Giuseppe Greco 0001, Krishna Manoorkar, Alessandra Palmigiano, Mattia Panettiere	Non-distributive Description Logic.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Dirk Pattinson, Nicola Olivetti, Cláudia Nalon	Resolution Calculi for Non-normal Modal Logics.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Bartosz Piotrowski, Ramon Fernández Mir, Edward W. Ayers	Machine-Learned Premise Selection for Lean.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Michael Rawson 0001, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel	Lemmas: Generation, Selection, Application.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Zuzana Haniková, Felip Manyà, Amanda Vidal	The MaxSAT Problem in the Real-Valued MV-Algebra.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Tim S. Lyon, Eugenio Orlandelli	Nested Sequents for Quantified Modal Logics.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Alexander V. Gheorghiu, Tao Gu, David J. Pym	Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Iris van der Giessen, Raheleh Jalali, Roman Kuznets	Extensions of K5: Proof Theory and Uniform Lyndon Interpolation.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Ian Shillito, Iris van der Giessen, Rajeev Goré, Rosalie Iemhoff	A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Andrzej Indrzejczak	Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Maurice Dekker, Johannes Kloibhofer, Johannes Marti, Yde Venema	Proof Systems for the Modal μ-Calculus Obtained by Determinizing Automata.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Boris Shminke	gym-saturation: Gymnasium Environments for Saturation Provers (System description).	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Anupam Das 0002, Sonia Marin	On Intuitionistic Diamonds (and Lack Thereof).	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Nicolas Peltier	Testing the Satisfiability of Formulas in Separation Logic with Permissions.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh, Lukas Zenger	Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Matteo Acclavio, Davide Catta, Federico Olimpieri	Canonicity of Proofs in Constructive Modal Logic.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Alexis Saurin	A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Andrzej Indrzejczak, Nils Kürbis	A Cut-Free, Sound and Complete Russellian Theory of Definite Descriptions.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Frank S. de Boer, Hans-Dieter A. Hiep, Stijn de Gouw	The Logic of Separation Logic: Models and Proofs.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Timo Lang	Some Analytic Systems of Rules.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Tiziano Dalmonte, Andrea Mazzullo	CoNP Complexity for Combinations of Non-normal Modal Logics.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Asta Halkjær From, Jørgen Villadsen	A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48	Clemens Eisenhofer, Ruba Alassaf, Michael Rawson 0001, Laura Kovács	Non-Classical Logics in Satisfiability Modulo Theories.	TABLEAUX	2023	DBLP DOI BibTeX RDF
48		Preface.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Leo Repp, Mario Frank 0002	nanoCoP-Omega: A Non-Clausal Connection Prover with Arithmetic.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Sean B. Holden	Connect++: A New Automated Theorem Prover Based on the Connection Calculus.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Jens Otten, Sean B. Holden	A Syntax for Connection Proofs.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Wolfgang Bibel	Comparison of Proof Methods.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Clemens Eisenhofer, Laura Kovács, Michael Rawson 0001	Embedding the Connection Calculus in Satisfiability Modulo Theories.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Christoph Wernhard	Structure-Generating First-Order Theorem Proving.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Jens Otten	20 Years of leanCoP - An Overview of the Provers.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Fredrik Rømming, Jens Otten, Sean B. Holden	Connections: Markov Decision Processes for Classical, Intuitionistic and Modal Connection Calculi.	AReCCa@TABLEAUX	2023	DBLP BibTeX RDF
48	Anupam Das 0002, Sara Negri (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Rajeev Goré, Revantha Ramanayake, Ian Shillito	Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Jan Rooduijn	Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Nils Kürbis	Proof-Theory and Semantics for a Theory of Definite Descriptions.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban	Learning Theorem Proving Components.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Tim S. Lyon	Nested Sequents for Intuitionistic Modal Logics via Structural Refinement.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Johannes Marti, Yde Venema	A Focus System for the Alternation-Free μ-Calculus.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Vitor Greati, Sérgio Marcelino, João Marcos 0001	Proof Search on Bilateralist Judgments over Non-deterministic Semantics.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Arnon Avron	Basing Sequent Systems on Exclusive-Or.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Björn Lellmann	From Input/Output Logics to Conditional Logics via Sequents - with Provers.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban	Towards Finding Longer Proofs.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Michael Mendler, Stephan Scheele, Luke Burke	The Došen Square Under Construction: A Tale of Four Modalities.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Jens Otten	The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Matteo Acclavio, Davide Catta, Lutz Straßburger	Game Semantics for Constructive Modal Logic.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Zsolt Zombori, Josef Urban, Miroslav Olsák	The Role of Entropy in Guiding a Connection Prover.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Bahareh Afshari, Graham E. Leigh, Guillermo Menéndez Turata	Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Tiziano Dalmonte, Charles Grellois, Nicola Olivetti	Terminating Calculi and Countermodels for Constructive Modal Logics.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Michael Rawson 0001, Giles Reger	Eliminating Models During Model Elimination.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	André Duarte 0002, Konstantin Korovin	AC Simplifications and Closure Redundancies in the Superposition Calculus.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Caitlin D'Abrera, Jeremy E. Dawson, Rajeev Goré	A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Michael Rawson 0001, Giles Reger	lazyCoP: Lazy Paramodulation Meets Neurally Guided Search.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Stepan L. Kuznetsov	Complexity of a Fragment of Infinitary Action Logic with Exponential via Non-well-founded Proofs.	TABLEAUX	2021	DBLP DOI BibTeX RDF
48	Serenella Cerrito, Andrei Popescu 0001 (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Simon Docherty, Reuben N. S. Rowe	A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Daniel Gâinâ, Ionut Tutu	Birkhoff Completeness for Hybrid-Dynamic First-Order Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Elaine Pimentel, Revantha Ramanayake, Björn Lellmann	Sequentialising Nested Systems.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Ioana Leustean, Natalia Moanga, Traian-Florin Serbanuta	Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Benjamin Ralph, Lutz Straßburger	Towards a Combinatorial Proof Theory.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Agata Ciabattoni, Timo Lang, Revantha Ramanayake	Bounded Sequent Calculi for Non-classical Logics via Hypersequents.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Abhishek De 0001, Alexis Saurin	Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Luca Geatti, Nicola Gigante, Angelo Montanari	A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Timo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller	A Game Model for Proofs with Costs.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Gabriel Ebner	Herbrand Constructivization for Automated Intuitionistic Theorem Proving.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Björn Lellmann	Combining Monotone and Normal Modal Logic in Nested Sequents - with Countermodels.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Eduard Kamburjan	Behavioral Program Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Chu Min Li, Felip Manyà, Joan Ramon Soler	A Tableau Calculus for Non-clausal Maximum Satisfiability.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban	ENIGMAWatch: ProofWatch Meets ENIGMA.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Anthony Lick	A Hypersequent Calculus with Clusters for Data Logic over Ordinals.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Didier Galmiche, Michel Marti, Daniel Méry	Relating Labelled and Label-Free Bunched Calculi in BI Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Matteo Acclavio, Lutz Straßburger	On Combinatorial Proofs for Modal Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	João G. Martins, André Platzer, João Leite 0001	Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Rajeev Goré, Björn Lellmann	Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Mnacho Echenim, Radu Iosif, Nicolas Peltier	Prenex Separation Logic with One Selector Field.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand	A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Yotam Dvir, Arnon Avron	First-Order Quasi-canonical Proof Systems.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Rémi Nollet, Alexis Saurin, Christine Tasson	PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points.	TABLEAUX	2019	DBLP DOI BibTeX RDF
48	Renate A. Schmidt, Cláudia Nalon (eds.)	Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Marianna Girlando, Björn Lellmann, Nicola Olivetti, Gian Luca Pozzato	Hypersequent Calculi for Lewis' Conditional Logics with Uniformity and Reflexivity.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	David M. Cerna, Michael Peter Lettmann	Integrating a Global Induction Mechanism into a Sequent Calculus.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Anupam Das 0002, Damien Pous	A Cut-Free Cyclic Proof System for Kleene Algebra.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Jens Otten	Non-clausal Connection Calculi for Non-classical Logics.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa	Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Peter H. Schmitt	A Mechanizable First-Order Theory of Ordinals.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Sonia Marin, Lutz Straßburger	Proof Theory for Indexed Nested Sequents.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Jeremy E. Dawson, Rajeev Goré	Issues in Machine-Checking the Decidability of Implicational Ticket Entailment.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Liron Cohen 0001	Completeness for Ancestral Logic via a Computationally-Meaningful Semantics.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Mateus de Oliveira Oliveira	Parameterized Provability in Equational Logic.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Sorin Stratulat	Cyclic Proofs with Ordering Constraints.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Dmitry Tishkovsky, Renate A. Schmidt	Rule Refinement for Semantic Tableau Calculi.	TABLEAUX	2017	DBLP DOI BibTeX RDF
48	Camillo Fiorentini, Mauro Ferrari 0002	A Forward Unprovability Calculus for Intuitionistic Propositional Logic.	TABLEAUX	2017	DBLP DOI BibTeX RDF