Christoph Weidenbach

Proceedings of the 35th International Workshop on Description Logics (DL 2022) co-located with Federated Logic Conference (FLoC 2022), 2022

Semantic Relevance.

[BibT_eX]

[DOI]

Fajar Haifani

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Connection-Minimal Abduction in EL via Translation to FOL.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

An Efficient Subsumption Test Pipeline for BS(LRA) Clauses.

[BibT_eX]

[DOI]

Lorenz Leutgeb

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories.

[BibT_eX]

[DOI]

Alberto Fiori

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic.

[BibT_eX]

[DOI]

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

Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance.

[BibT_eX]

[DOI]

Fajar Haifani

Sophie Tourret

Proceedings of the Automated Deduction - CADE 28, 2021

2020

A complete and terminating approach to linear integer solving.

[BibT_eX]

[DOI]

Thomas Sturm

J. Symb. Comput., 2020

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Preface to the Special Issue on Automated Reasoning Systems.

[BibT_eX]

[DOI]

Armin Biere

Cesare Tinelli

J. Autom. Reason., 2020

SCL with Theory Constraints.

[BibT_eX]

[DOI]

Alberto Fiori

CoRR, 2020

A Verified SAT Solver Framework including Optimization and Partial Valuations.

[BibT_eX]

[DOI]

Mathias Fleury

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, 2020

On a Notion of Relevance.

[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

The Challenge of Unifying Semantic and Syntactic Inference Restrictions.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Automated Reasoning: Challenges, 2019

On the Expressivity and Applicability of Model Representation Formalisms.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

SCL Clause Learning from Simple Models.

[BibT_eX]

[DOI]

Alberto Fiori

Proceedings of the Automated Deduction - CADE 27, 2019

SPASS-SATT - A CDCL(LA) Solver.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

A machine-checked correctness proof for Pastry.

[BibT_eX]

[DOI]

Noran Azmy

Sci. Comput. Program., 2018

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.

[BibT_eX]

[DOI]

Mathias Fleury

Peter Lammich

J. Autom. Reason., 2018

2017

BDI: a new decidable clause class.

[BibT_eX]

[DOI]

Manuel Lamotte-Schubert

J. Log. Comput., 2017

Preface - Special Issue of Selected Extended Papers of IJCAR 2014.

[BibT_eX]

[DOI]

Stéphane Demri

Deepak Kapur

J. Autom. Reason., 2017

New techniques for linear arithmetic: cubes and equalities.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable.

[BibT_eX]

[DOI]

CoRR, 2017

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.

[BibT_eX]

[DOI]

Mathias Fleury

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Do Portfolio Solvers Harm?

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated.

[BibT_eX]

[DOI]

Thomas Sturm

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Compliance, Functional Safety and Fault Detection by Formal Methods.

[BibT_eX]

[DOI]

Christof Fetzer

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Ordered Resolution with Straight Dismatching Constraints.

[BibT_eX]

[DOI]

Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 2016

A Dynamic Logic for Configuration.

[BibT_eX]

[DOI]

Ching Hoo Tang

Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., 2016

Computing a Complete Basis for Equalities Implied by a System of LRA Constraints.

[BibT_eX]

[DOI]

Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, 2016

Fast Cube Tests for LIA Constraint Solving.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Rigorous Correctness Proof for Pastry.

[BibT_eX]

[DOI]

Noran Azmy

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015

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

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Viorica Sofronie-Stokkermans

Dagstuhl Reports, 2015

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete.

[BibT_eX]

[DOI]

CoRR, 2015

First-Order Logic Theorem Proving via Counterexample-Guided Abstraction Refinement.

[BibT_eX]

[DOI]

CoRR, 2015

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper).

[BibT_eX]

[DOI]

Gábor Alagi

CoRR, 2015

Model-Based Variant Management with v.control.

[BibT_eX]

[DOI]

Proceedings of the Transdisciplinary Lifecycle Analysis of Systems, 2015

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation.

[BibT_eX]

[DOI]

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

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment.

[BibT_eX]

[DOI]

Gábor Alagi

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

Linear Integer Arithmetic Revisited.

[BibT_eX]

[DOI]

Thomas Sturm

Proceedings of the Automated Deduction - CADE-25, 2015

Automated Reasoning Building Blocks.

[BibT_eX]

[DOI]

Proceedings of the Correct System Design, 2015

2013

Deduction and Arithmetic (Dagstuhl Seminar 13411).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2013

Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material).

[BibT_eX]

[DOI]

CoRR, 2013

BDI: A New Decidable First-order Clause Class.

[BibT_eX]

[DOI]

Manuel Lamotte-Schubert

Proceedings of the LPAR 2013, 2013

Automated verification of interactive rule-based configuration systems.

[BibT_eX]

[DOI]

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Computing Tiny Clause Normal Forms.

[BibT_eX]

[DOI]

Noran Azmy

Proceedings of the Automated Deduction - CADE-24, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.

[BibT_eX]

[DOI]

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

Superposition for Bounded Domains.

[BibT_eX]

[DOI]

Thomas Hillenbrand

Proceedings of the Automated Reasoning and Mathematics, 2013

From Search to Computation: Redundancy Criteria and Simplification at Work.

[BibT_eX]

[DOI]

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

2012

Superposition Decides the First-Order Logic Fragment Over Ground Theories.

[BibT_eX]

[DOI]

Evgeny Kruglov

Math. Comput. Sci., 2012

Superposition as a Decision Procedure for Timed Automata.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2012

Labelled Superposition for PLTL.

[BibT_eX]

[DOI]

Martin Suda

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Automatic Generation of Invariants for Circular Derivations in SUP(LA).

[BibT_eX]

[DOI]

Evgeny Kruglov

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.

[BibT_eX]

[DOI]

Andrei Popescu

Daniel Wand

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Satisfiability Checking and Query Answering for Large Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.

[BibT_eX]

[DOI]

Martin Suda

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Combination of Disjoint Theories: Beyond Decidability.

[BibT_eX]

[DOI]

Pascal Fontaine

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Superposition Modulo Non-linear Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Towards Verification of the Pastry Protocol Using TLA + .

[BibT_eX]

[DOI]

Tianxiang Lu

Proceedings of the Formal Techniques for Distributed Systems, 2011

2010

Superposition for fixed domains.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

Subterm contextual rewriting.

[BibT_eX]

[DOI]

AI Commun., 2010

Superposition-Based Analysis of First-Order Probabilistic Timed Automata.

[BibT_eX]

[DOI]

Holger Hermanns

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

On the Saturation of YAGO.

[BibT_eX]

[DOI]

Martin Suda

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

2009

Labelled splitting.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

Analysis of Authorizations in SAP R/3.

[BibT_eX]

[DOI]

Manuel Lamotte-Schubert

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

Superposition Modulo Linear Arithmetic SUP(LA).

[BibT_eX]

[DOI]

Ernst Althaus

Evgeny Kruglov

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

SPASS Version 3.5.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

Decidability Results for Saturation-Based Model Building.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Contextual Rewriting in SPASS.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, 2008

2007

System Description: SpassVersion 3.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

Labelled Clauses.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2002

S PASS Version 2.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

First-Order Atom Definitions Extended.

[BibT_eX]

[DOI]

Bijan Afshordel

Thomas Hillenbrand

Proceedings of the Logic for Programming, 2001

Combining Superposition, Sorts and Splitting.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Computing Small Clause Normal Forms.

[BibT_eX]

[DOI]

Andreas Nonnengart

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

1999

MSPASS: Subsumption Testing with SPASS.

[BibT_eX]

[DOI]

Ullrich Hustadt

Renate A. Schmidt

Proceedings of the 1999 International Workshop on Description Logics (DL'99), Linköping, Sweden, July 30, 1999

System Description: Spass Version 1.0.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

Towards an Automatic Analysis of Security Protocols in First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Paradigmen und Perspektiven der automatischen Deduktion.

[BibT_eX]

Reinhold Letz

Künstliche Intell., 1998

Unification in Extension of Shallow Equational Theories.

[BibT_eX]

[DOI]

Florent Jacquemard

Christoph Meyer

Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

On Generating Small Clause Normal Forms.

[BibT_eX]

[DOI]

Andreas Nonnengart

Georg Rock

Proceedings of the Automated Deduction, 1998

1997

SPASS - Version 0.49.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

Soft Typing for Ordered Resolution.

[BibT_eX]

[DOI]

Harald Ganzinger

Christoph Meyer

Proceedings of the Automated Deduction, 1997

1996

Unification in Sort Theories and Its Applications.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 1996

SPASS & FLOTTER Version 0.42.

[BibT_eX]

[DOI]

Bernd Gaede

Georg Rock

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Unification in Pseudo-Linear Sort Theories is Decidable.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Computational aspects of a first-order logic with sorts.

[BibT_eX]

[DOI]

PhD thesis, 1996

1995

A Note on Assumptions about Skolem Functions.

[BibT_eX]

[DOI]

Hans Jürgen Ohlbach

J. Autom. Reason., 1995

First-Order Tableaux with Sorts.

[BibT_eX]

[DOI]

Log. J. IGPL, 1995

1993

Extending the Resolution Method with Sorts.

[BibT_eX]

[DOI]

Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

1992

Deduktionssysteme.

[BibT_eX]

Manfred Kerber

Künstliche Intell., 1992

A New Sorted Logic.

[BibT_eX]

[DOI]

Proceedings of the GWAI-92: Advances in Artificial Intelligence, 16th German Conference on Artificial Intelligence, Bonn, Germany, August 31, 1992

1990

A Resolution Calculus with Dynamic Sort Structures and Partial Functions.

[BibT_eX]