Viorica Sofronie-Stokkermans

On Testing Containedness Between Geometric Graph Classes using Second-order Quantifier Elimination and Hierarchical Reasoning (Short Paper).

[BibT_eX]

[DOI]

Lucas Böltz

Hannes Frey

Symbol Elimination and Applications to Parametric Entailment Problems.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

2020

Parametric Systems: Verification and Synthesis.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2020

Measuring Disagreement with Interpolants.

[BibT_eX]

[DOI]

Jandson S. Ribeiro

Matthias Thimm

Proceedings of the Scalable Uncertainty Management - 14th International Conference, 2020

Finding High-Level Explanations for Subsumption w.r.t. Combinations of CBoxes in EL and EL+.

[BibT_eX]

[DOI]

Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), 2020

2019

On Invariant Synthesis for Parametric Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

On Interpolation and Symbol Elimination in Theory Extensions.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

On Inductive Verification and Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Selected Student Contributions and Workshop Papers of LuxLogAI 2018, 2018

2017

Representation Theorems and Locality for Subsumption Testing and Interpolation in the Description Logics ɛℒ, ɛℒ+ and their Extensions with n-ary Roles and Numerical Domains.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Fundam. Informaticae, 2017

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371).

[BibT_eX]

[DOI]

Carsten Fuhs

Cesare Tinelli

Dagstuhl Reports, 2017

Decision Procedures for Theories of Sets with Measures.

[BibT_eX]

[DOI]

Markus Bender

Jasmin Christian Blanchette

Proceedings of the Automated Deduction - CADE 26, 2017

2015

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381).

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Christoph Weidenbach

Dagstuhl Reports, 2015

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata.

[BibT_eX]

[DOI]

Werner Damm

Matthias Horbach

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

On First-Order Model-Based Reasoning.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Ulrich Furbach

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

Hierarchical Reasoning in Local Theory Extensions and Applications.

[BibT_eX]

[DOI]

Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014

Locality Transfer: From Constrained Axiomatizations to Reachability Predicates.

[BibT_eX]

[DOI]

Matthias Horbach

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Preface: Special Issue of Selected Extended Papers of CADE-23.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

J. Autom. Reason., 2013

Locality and Applications to Subsumption Testing in EL and Some of its Extensions.

[BibT_eX]

[DOI]

Sci. Ann. Comput. Sci., 2013

Locality and applications to subsumption testing and interpolation in $\mathcal{EL}$ and some of its extensions.

[BibT_eX]

[DOI]

CoRR, 2013

Obtaining Finite Local Theory Axiomatizations via Saturation.

[BibT_eX]

[DOI]

Matthias Horbach

Proceedings of the Frontiers of Combining Systems, 2013

Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

On Combinations of Local Theory Extensions.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

First-order theorem proving: Foreword.

[BibT_eX]

[DOI]

Nicolas Peltier

J. Symb. Comput., 2012

2011

PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata.

[BibT_eX]

[DOI]

Werner Damm

Math. Comput. Sci., 2011

Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata.

[BibT_eX]

[DOI]

Werner Damm

Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0.

[BibT_eX]

[DOI]

Francis Gasse

Proceedings of the 24th International Workshop on Description Logics (DL 2011), 2011

2010

Constraint solving for interpolation.

[BibT_eX]

[DOI]

Andrey Rybalchenko

J. Symb. Comput., 2010

Special issue on automated deduction: Decidability, complexity, tractability.

[BibT_eX]

[DOI]

Silvio Ghilardi

Ulrike Sattler

Ashish Tiwari

J. Symb. Comput., 2010

System Description: H-PILoT (Version 1.9)

[BibT_eX]

[DOI]

CoRR, 2010

Automatic Verification of Parametric Specifications with Complex Topologies.

[BibT_eX]

[DOI]

Johannes Faber

Proceedings of the Integrated Formal Methods - 8th International Conference, 2010

Hierarchical Reasoning for the Verification of Parametric Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

On Hierarchical Reasoning in Combinations of Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Preface.

[BibT_eX]

[DOI]

Nicolas Peltier

Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms.

[BibT_eX]

[DOI]

Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

Locality Results for Certain Extensions of Theories with Bridging Functions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

System Description: H-PILoT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Interpolation in Local Theory Extensions.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2008

On Local Reasoning in Verification.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Efficient Hierarchical Reasoning about Functions over Numerical Domains.

[BibT_eX]

[DOI]

Proceedings of the KI 2008: Advances in Artificial Intelligence, 2008

Locality and subsumption testing in EL and some of its extensions.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 7, 2008

2007

On unification for bounded distributive lattices.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2007

Automated Reasoning in Some Local Extensions of Ordered Structures.

[BibT_eX]

[DOI]

J. Multiple Valued Log. Soft Comput., 2007

Automated theorem proving by resolution in non-classical logics.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2007

Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters.

[BibT_eX]

[DOI]

Johannes Faber

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

Local Theory Extensions, Hierarchical Reasoning and Applications to Verification.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

2006

Modular proof systems for partial functions with Evans equality.

[BibT_eX]

[DOI]

Harald Ganzinger

Uwe Waldmann

Inf. Comput., 2006

Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems.

[BibT_eX]

[DOI]

Proceedings of the Workshops on Geometric and Topological Methods in Concurrency Theory, 2006

Applications of Hierarchical Reasoning in the Verification of Complex Systems.

[BibT_eX]

[DOI]

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

2005

Hierarchic Reasoning in Local Theory Extensions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

Resolution-Based Decision Procedures for the Positive Theory of Some Finitely Generated Varieties of Algebras.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2004), 2004

Modular Proof Systems for Partial Functions with Weak Equality.

[BibT_eX]

[DOI]

Harald Ganzinger

Uwe Waldmann

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators.

[BibT_eX]

[DOI]

J. Symb. Comput., 2003

2002

On Uniform Word Problems Involving Bridging Operators on Distributive Lattices.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

2001

Representation Theorems and the Semantics of (Semi)Lattice-Based Logics.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, 2001

2000

Duality and Canonical Extensions of Bounded Distributive Lattices with Operators, and Applications to the Semantics of Non-Classical Logics II.

[BibT_eX]

[DOI]

Stud Logica, 2000

Duality and Canonical Extensions of Bounded Distributive Lattices with Operators, and Applications to the Semantics of Non-Classical Logics I.

[BibT_eX]

[DOI]

Stud Logica, 2000

Chaining Techniques for Automated Theorem Proving in Many-Valued Logics.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic, 2000

On Unification for Bonded Distributive Lattices.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1999

Representation Theorems and Theorem Proving in Non-Classical Logics.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

Modeling Interaction by Sheaves and Geometric Logic.

[BibT_eX]

[DOI]

Karel Stokkermans

Proceedings of the Fundamentals of Computation Theory, 12th International Symposium, 1999

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Resolution-Based Theorem Proving for SHn-Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

On Translation of Finitely-Valued Logics to Classical First-Order Logic.

[BibT_eX]