A Resolution Calculus with Dynamic Sort Structures and Partial Functions. - Christoph Weidenbach; Hans Jürgen Ohlbach (ECAI, 1990)

A New Sorted Logic. - Christoph Weidenbach (GWAI, 1992)

Deduktionssysteme. - Manfred Kerber; Christoph Weidenbach (Künstliche Intell., 1992)

Extending the Resolution Method with Sorts. - Christoph Weidenbach (IJCAI, 1993)

First-Order Tableaux with Sorts. - Christoph Weidenbach (Log. J. IGPL, 1995)

A Note on Assumptions about Skolem Functions. - Hans Jürgen Ohlbach; Christoph Weidenbach (J. Autom. Reason., 1995)

Computational aspects of a first-order logic with sorts. - Christoph Weidenbach (1996)

Unification in Pseudo-Linear Sort Theories is Decidable. - Christoph Weidenbach (CADE, 1996)

SPASS & FLOTTER Version 0.42. - Christoph Weidenbach; Bernd Gaede; Georg Rock (CADE, 1996)

Unification in Sort Theories and Its Applications. - Christoph Weidenbach (Ann. Math. Artif. Intell., 1996)

Soft Typing for Ordered Resolution. - Harald Ganzinger; Christoph Meyer 001; Christoph Weidenbach (CADE, 1997)

SPASS - Version 0.49. - Christoph Weidenbach (J. Autom. Reason., 1997)

On Generating Small Clause Normal Forms. - Andreas Nonnengart; Georg Rock; Christoph Weidenbach (CADE, 1998)

Unification in Extension of Shallow Equational Theories. - Florent Jacquemard; Christoph Meyer 001; Christoph Weidenbach (RTA, 1998)

Paradigmen und Perspektiven der automatischen Deduktion. - Reinhold Letz; Christoph Weidenbach (Künstliche Intell., 1998)

Towards an Automatic Analysis of Security Protocols in First-Order Logic. - Christoph Weidenbach (CADE, 1999)

System Description: Spass Version 1.0.0. - Christoph Weidenbach (CADE, 1999)

MSPASS: Subsumption Testing with SPASS. - Ullrich Hustadt; Renate A. Schmidt; Christoph Weidenbach (Description Logics, 1999)

Computing Small Clause Normal Forms. - Andreas Nonnengart; Christoph Weidenbach (Handbook of Automated Reasoning, 2001)

Combining Superposition, Sorts and Splitting. - Christoph Weidenbach (Handbook of Automated Reasoning, 2001)

First-Order Atom Definitions Extended. - Bijan Afshordel; Thomas Hillenbrand; Christoph Weidenbach (LPAR, 2001)

S PASS Version 2.0. - Christoph Weidenbach; Uwe Brahm; Thomas Hillenbrand; Enno Keen; Christian Theobalt; Dalibor Topic (CADE, 2002)

Labelled Clauses. - Tal Lev-Ami; Christoph Weidenbach; Thomas W. Reps; Mooly Sagiv (CADE, 2007)

System Description: SpassVersion 3.0. - Christoph Weidenbach; Renate A. Schmidt; Thomas Hillenbrand; Rostislav Rusev; Dalibor Topic (CADE, 2007)

Contextual Rewriting in SPASS. - Christoph Weidenbach; Patrick Wischnewski (PAAR/ESHOL, 2008)

Decidability Results for Saturation-Based Model Building. - Matthias Horbach; Christoph Weidenbach (CADE, 2009)

SPASS Version 3.5. - Christoph Weidenbach; Dilyana Dimova; Arnaud Fietzke; Rohit Kumar; Martin Suda 001; Patrick Wischnewski (CADE, 2009)

Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries. - Matthias Horbach; Christoph Weidenbach (CSL, 2009)

Superposition Modulo Linear Arithmetic SUP(LA). - Ernst Althaus; Evgeny Kruglov; Christoph Weidenbach (FroCoS, 2009)

Analysis of Authorizations in SAP R/3. - Manuel Lamotte-Schubert; Christoph Weidenbach (FTP, 2009)

Labelled splitting. - Arnaud Fietzke; Christoph Weidenbach (Ann. Math. Artif. Intell., 2009)

On the Saturation of YAGO. - Martin Suda 001; Christoph Weidenbach; Patrick Wischnewski (IJCAR, 2010)

Superposition-Based Analysis of First-Order Probabilistic Timed Automata. - Arnaud Fietzke; Holger Hermanns; Christoph Weidenbach (LPAR (Yogyakarta), 2010)

Subterm contextual rewriting. - Christoph Weidenbach; Patrick Wischnewski (AI Commun., 2010)

Superposition for fixed domains. - Matthias Horbach; Christoph Weidenbach (ACM Trans. Comput. Log., 2010)

Towards Verification of the Pastry Protocol Using TLA + . - Tianxiang Lu; Stephan Merz; Christoph Weidenbach (FMOODS/FORTE, 2011)

Superposition Modulo Non-linear Arithmetic. - Andreas Eggers; Evgeny Kruglov; Stefan Kupferschmid; Karsten Scheibler; Tino Teige; Christoph Weidenbach (FroCoS, 2011)

Combination of Disjoint Theories: Beyond Decidability. - Pascal Fontaine; Stephan Merz; Christoph Weidenbach (IJCAR, 2012)

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. - Martin Suda 001; Christoph Weidenbach (IJCAR, 2012)

Satisfiability Checking and Query Answering for Large Ontologies. - Christoph Weidenbach; Patrick Wischnewski (PAAR@IJCAR, 2012)

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. - Jasmin Christian Blanchette; Andrei Popescu 001; Daniel Wand; Christoph Weidenbach (ITP, 2012)

Automatic Generation of Invariants for Circular Derivations in SUP(LA). - Arnaud Fietzke; Evgeny Kruglov; Christoph Weidenbach (LPAR, 2012)

Labelled Superposition for PLTL. - Martin Suda 001; Christoph Weidenbach (LPAR, 2012)

Superposition as a Decision Procedure for Timed Automata. - Arnaud Fietzke; Christoph Weidenbach (Math. Comput. Sci., 2012)

Superposition Decides the First-Order Logic Fragment Over Ground Theories. - Evgeny Kruglov; Christoph Weidenbach (Math. Comput. Sci., 2012)

From Search to Computation: Redundancy Criteria and Simplification at Work. - Thomas Hillenbrand; Ruzica Piskac; Uwe Waldmann; Christoph Weidenbach (Programming Logics, 2013)

Superposition for Bounded Domains. - Thomas Hillenbrand; Christoph Weidenbach (Automated Reasoning and Mathematics, 2013)

Harald Ganzinger's Legacy: Contributions to Logics and Programming. - Deepak Kapur; Robert Nieuwenhuis; Andrei Voronkov; Christoph Weidenbach; Reinhard Wilhelm (Programming Logics, 2013)

Computing Tiny Clause Normal Forms. - Noran Azmy; Christoph Weidenbach (CADE, 2013)

Automated verification of interactive rule-based configuration systems. - Deepak Dhungana; Ching Hoo Tang; Christoph Weidenbach; Patrick Wischnewski (ASE, 2013)

BDI: A New Decidable First-order Clause Class. - Manuel Lamotte-Schubert; Christoph Weidenbach (LPAR (short papers), 2013)

Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material). - Deepak Dhungana; Ching Hoo Tang; Christoph Weidenbach; Patrick Wischnewski (CoRR, 2013)

Deduction and Arithmetic (Dagstuhl Seminar 13411). - Nikolaj S. Bjørner; Reiner Hähnle; Tobias Nipkow; Christoph Weidenbach (Dagstuhl Reports, 2013)

Automated Reasoning Building Blocks. - Christoph Weidenbach (Correct System Design, 2015)

Linear Integer Arithmetic Revisited. - Martin Bromberger; Thomas Sturm 001; Christoph Weidenbach (CADE, 2015)

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. - Gábor Alagi; Christoph Weidenbach (FroCos, 2015)

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. - Andreas Teucke; Christoph Weidenbach (FroCos, 2015)

Model-Based Variant Management with v.control. - Christopher Junk; Robert Rößger; Georg Rock; Karsten Theis; Christoph Weidenbach; Patrick Wischnewski (CE, 2015)

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper). - Gábor Alagi; Christoph Weidenbach (CoRR, 2015)

First-Order Logic Theorem Proving via Counterexample-Guided Abstraction Refinement. - Andreas Teucke; Christoph Weidenbach (CoRR, 2015)

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. - Marco Voigt; Christoph Weidenbach (CoRR, 2015)

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). - Nikolaj S. Bjørner; Jasmin Christian Blanchette; Viorica Sofronie-Stokkermans; Christoph Weidenbach (Dagstuhl Reports, 2015)

A Rigorous Correctness Proof for Pastry. - Noran Azmy; Stephan Merz; Christoph Weidenbach (ABZ, 2016)

Fast Cube Tests for LIA Constraint Solving. - Martin Bromberger; Christoph Weidenbach (IJCAR, 2016)

Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. - Martin Bromberger; Christoph Weidenbach (SMT@IJCAR, 2016)

A Dynamic Logic for Configuration. - Ching Hoo Tang; Christoph Weidenbach (ARQNL@IJCAR, 2016)

Ordered Resolution with Straight Dismatching Constraints. - Andreas Teucke; Christoph Weidenbach (PAAR@IJCAR, 2016)

Compliance, Functional Safety and Fault Detection by Formal Methods. - Christof Fetzer; Christoph Weidenbach; Patrick Wischnewski (ISoLA (2), 2016)

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. - Thomas Sturm 001; Marco Voigt; Christoph Weidenbach (LICS, 2016)

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. - Matthias Horbach; Marco Voigt; Christoph Weidenbach (CADE, 2017)

Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. - Andreas Teucke; Christoph Weidenbach (CADE, 2017)

Do Portfolio Solvers Harm? - Christoph Weidenbach (ARCADE@CADE, 2017)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Christoph Weidenbach (IJCAI, 2017)

The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. - Matthias Horbach; Marco Voigt; Christoph Weidenbach (CoRR, 2017)

New techniques for linear arithmetic: cubes and equalities. - Martin Bromberger; Christoph Weidenbach (Formal Methods Syst. Des., 2017)

Preface - Special Issue of Selected Extended Papers of IJCAR 2014. - Stéphane Demri; Deepak Kapur; Christoph Weidenbach (J. Autom. Reason., 2017)

BDI: a new decidable clause class. - Manuel Lamotte-Schubert; Christoph Weidenbach (J. Log. Comput., 2017)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Peter Lammich; Christoph Weidenbach (J. Autom. Reason., 2018)

A machine-checked correctness proof for Pastry. - Noran Azmy; Stephan Merz; Christoph Weidenbach (Sci. Comput. Program., 2018)

SPASS-SATT - A CDCL(LA) Solver. - Martin Bromberger; Mathias Fleury; Simon Schwarz; Christoph Weidenbach (CADE, 2019)

SCL Clause Learning from Simple Models. - Alberto Fiori; Christoph Weidenbach (CADE, 2019)

On the Expressivity and Applicability of Model Representation Formalisms. - Andreas Teucke; Marco Voigt; Christoph Weidenbach (FroCos, 2019)

The Challenge of Unifying Semantic and Syntactic Inference Restrictions. - Christoph Weidenbach (ARCADE@CADE, 2019)

On a Notion of Relevance. - Fajar Haifani; Patrick Koopmann; Sophie Tourret; Christoph Weidenbach (Description Logics, 2020)

Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. - Rasha Faqeh; Christof Fetzer; Holger Hermanns; Jörg Hoffmann 001; Michaela Klauck; Maximilian A. Köhl; Marcel Steinmetz; Christoph Weidenbach (ISoLA (2), 2020)

A Verified SAT Solver Framework including Optimization and Partial Valuations. - Mathias Fleury; Christoph Weidenbach (LPAR, 2020)

SCL with Theory Constraints. - Alberto Fiori; Christoph Weidenbach (CoRR, 2020)

Preface to the Special Issue on Automated Reasoning Systems. - Armin Biere; Cesare Tinelli; Christoph Weidenbach (J. Autom. Reason., 2020)

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. - Andreas Teucke; Christoph Weidenbach (J. Autom. Reason., 2020)

A complete and terminating approach to linear integer solving. - Martin Bromberger; Thomas Sturm 001; Christoph Weidenbach (J. Symb. Comput., 2020)

Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. - Fajar Haifani; Sophie Tourret; Christoph Weidenbach (CADE, 2021)

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. - Martin Bromberger; Irina Dragoste; Rasha Faqeh; Christof Fetzer; Markus Krötzsch; Christoph Weidenbach (FroCoS, 2021)

Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. - Martin Bromberger; Alberto Fiori; Christoph Weidenbach (VMCAI, 2021)

An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. - Martin Bromberger; Lorenz Leutgeb; Christoph Weidenbach (IJCAR, 2022)

Connection-Minimal Abduction in EL via Translation to FOL. - Fajar Haifani; Patrick Koopmann; Sophie Tourret; Christoph Weidenbach (IJCAR, 2022)

Semantic Relevance. - Fajar Haifani; Christoph Weidenbach (IJCAR, 2022)

Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract). - Fajar Haifani; Patrick Koopmann; Sophie Tourret; Christoph Weidenbach (Description Logics, 2022)

A Two-Watched Literal Scheme for First-Order Logic. - Martin Bromberger; Tobias Gehl; Lorenz Leutgeb; Christoph Weidenbach (PAAR@IJCAR, 2022)

A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. - Martin Bromberger; Irina Dragoste; Rasha Faqeh; Christof Fetzer; Larry González; Markus Krötzsch; Maximilian Marx 001; Harish K. Murali; Christoph Weidenbach (TACAS (1), 2022)

Connection-minimal Abduction in EL via Translation to FOL - Technical Report. - Fajar Haifani; Patrick Koopmann; Sophie Tourret; Christoph Weidenbach (CoRR, 2022)

A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. - Sophie Tourret; Christoph Weidenbach (J. Autom. Reason., 2022)

An Isabelle/HOL Formalization of the SCL(FOL) Calculus. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2023)

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. - Martin Bromberger; Chaahat Jain; Christoph Weidenbach (CADE, 2023)

KBO Constraint Solving Revisited. - Yasmine Briefs; Hendrik Leidinger; Christoph Weidenbach (FroCoS, 2023)

Symbolic Model Construction for Saturated Constrained Horn Clauses. - Martin Bromberger; Lorenz Leutgeb; Christoph Weidenbach (FroCoS, 2023)

Exploring Partial Models with SCL. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (LPAR, 2023)

SCL(FOL) Revisited. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (CoRR, 2023)

SCL(EQ): SCL for First-Order Logic with Equality. - Hendrik Leidinger; Christoph Weidenbach (J. Autom. Reason., 2023)

First-Order Automatic Literal Model Generation. - Martin Bromberger; Florent Krasnopol; Sibylle Möhle; Christoph Weidenbach (IJCAR (1), 2024)

Automatic Bit- and Memory-Precise Verification of eBPF Code. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (LPAR, 2024)

Non-Ground Congruence Closure. - Hendrik Leidinger; Christoph Weidenbach (CoRR, 2024)

A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2025)

Computing Ground Congruence Classes. - Hendrik Leidinger; Christoph Weidenbach (CADE, 2025)