![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Christoph Weidenbach
Person information
- affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 1996
- [b1]Christoph Weidenbach:
Computational aspects of a first-order logic with sorts. Saarland University, Saarbrücken, Germany, 1996, pp. I-XIII, 1-183
Journal Articles
- 2023
- [j21]Hendrik Leidinger, Christoph Weidenbach:
SCL(EQ): SCL for First-Order Logic with Equality. J. Autom. Reason. 67(3): 22 (2023) - 2022
- [j20]Sophie Tourret, Christoph Weidenbach
:
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. J. Autom. Reason. 66(4): 575-584 (2022) - 2020
- [j19]Armin Biere
, Cesare Tinelli
, Christoph Weidenbach
:
Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. 64(3): 361-362 (2020) - [j18]Andreas Teucke, Christoph Weidenbach
:
SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. J. Autom. Reason. 64(3): 611-640 (2020) - [j17]Martin Bromberger, Thomas Sturm, Christoph Weidenbach:
A complete and terminating approach to linear integer solving. J. Symb. Comput. 100: 102-136 (2020) - 2018
- [j16]Jasmin Christian Blanchette
, Mathias Fleury, Peter Lammich
, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61(1-4): 333-365 (2018) - [j15]Noran Azmy, Stephan Merz
, Christoph Weidenbach:
A machine-checked correctness proof for Pastry. Sci. Comput. Program. 158: 64-80 (2018) - 2017
- [j14]Martin Bromberger
, Christoph Weidenbach:
New techniques for linear arithmetic: cubes and equalities. Formal Methods Syst. Des. 51(3): 433-461 (2017) - [j13]Stéphane Demri, Deepak Kapur, Christoph Weidenbach
:
Preface - Special Issue of Selected Extended Papers of IJCAR 2014. J. Autom. Reason. 58(1): 1-2 (2017) - [j12]Manuel Lamotte-Schubert, Christoph Weidenbach:
BDI: a new decidable clause class. J. Log. Comput. 27(2): 441-468 (2017) - 2012
- [j11]Arnaud Fietzke, Christoph Weidenbach:
Superposition as a Decision Procedure for Timed Automata. Math. Comput. Sci. 6(4): 409-425 (2012) - [j10]Evgeny Kruglov, Christoph Weidenbach:
Superposition Decides the First-Order Logic Fragment Over Ground Theories. Math. Comput. Sci. 6(4): 427-456 (2012) - 2010
- [j9]Christoph Weidenbach, Patrick Wischnewski:
Subterm contextual rewriting. AI Commun. 23(2-3): 97-109 (2010) - [j8]Matthias Horbach, Christoph Weidenbach:
Superposition for fixed domains. ACM Trans. Comput. Log. 11(4): 27:1-27:35 (2010) - 2009
- [j7]Arnaud Fietzke, Christoph Weidenbach:
Labelled splitting. Ann. Math. Artif. Intell. 55(1-2): 3-34 (2009) - 1998
- [j6]Reinhold Letz, Christoph Weidenbach:
Paradigmen und Perspektiven der automatischen Deduktion. Künstliche Intell. 12(4): 15-19 (1998) - 1997
- [j5]Christoph Weidenbach:
SPASS - Version 0.49. J. Autom. Reason. 18(2): 247-252 (1997) - 1996
- [j4]Christoph Weidenbach:
Unification in Sort Theories and Its Applications. Ann. Math. Artif. Intell. 18(2-4): 261-293 (1996) - 1995
- [j3]Christoph Weidenbach:
First-Order Tableaux with Sorts. Log. J. IGPL 3(6): 887-906 (1995) - [j2]Hans Jürgen Ohlbach, Christoph Weidenbach:
A Note on Assumptions about Skolem Functions. J. Autom. Reason. 15(2): 267-275 (1995) - 1992
- [j1]Manfred Kerber, Christoph Weidenbach:
Deduktionssysteme. Künstliche Intell. 6(3): 14-22 (1992)
Conference and Workshop Papers
- 2024
- [c81]Martin Bromberger, Florent Krasnopol, Sibylle Möhle, Christoph Weidenbach:
First-Order Automatic Literal Model Generation. IJCAR (1) 2024: 133-153 - [c80]Martin Bromberger, Simon Schwarz, Christoph Weidenbach:
Automatic Bit- and Memory-Precise Verification of eBPF Code. LPAR 2024: 198-221 - 2023
- [c79]Martin Bromberger
, Martin Desharnais
, Christoph Weidenbach
:
An Isabelle/HOL Formalization of the SCL(FOL) Calculus. CADE 2023: 116-133 - [c78]Martin Bromberger, Chaahat Jain, Christoph Weidenbach:
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CADE 2023: 134-152 - [c77]Yasmine Briefs
, Hendrik Leidinger
, Christoph Weidenbach
:
KBO Constraint Solving Revisited. FroCoS 2023: 81-98 - [c76]Martin Bromberger
, Lorenz Leutgeb
, Christoph Weidenbach
:
Symbolic Model Construction for Saturated Constrained Horn Clauses. FroCoS 2023: 137-155 - [c75]Martin Bromberger, Simon Schwarz, Christoph Weidenbach:
Exploring Partial Models with SCL. LPAR 2023: 48-72 - 2022
- [c74]Martin Bromberger
, Lorenz Leutgeb
, Christoph Weidenbach
:
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. IJCAR 2022: 147-168 - [c73]Fajar Haifani
, Patrick Koopmann
, Sophie Tourret
, Christoph Weidenbach
:
Connection-Minimal Abduction in EL via Translation to FOL. IJCAR 2022: 188-207 - [c72]Fajar Haifani
, Christoph Weidenbach
:
Semantic Relevance. IJCAR 2022: 208-227 - [c71]Hendrik Leidinger
, Christoph Weidenbach
:
SCL(EQ): SCL for First-Order Logic with Equality. IJCAR 2022: 228-247 - [c70]Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach:
Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract). Description Logics 2022 - [c69]Martin Bromberger, Tobias Gehl, Lorenz Leutgeb, Christoph Weidenbach:
A Two-Watched Literal Scheme for First-Order Logic. PAAR@IJCAR 2022 - [c68]Martin Bromberger, Simon Schwarz, Christoph Weidenbach:
Exploring Partial Models with SCL. PAAR@IJCAR 2022 - [c67]Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx
, Harish K. Murali, Christoph Weidenbach:
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. TACAS (1) 2022: 480-501 - 2021
- [c66]Fajar Haifani
, Sophie Tourret
, Christoph Weidenbach
:
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. CADE 2021: 327-343 - [c65]Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach:
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. FroCoS 2021: 3-24 - [c64]Martin Bromberger, Alberto Fiori, Christoph Weidenbach:
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. VMCAI 2021: 511-533 - 2020
- [c63]Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach:
On a Notion of Relevance. Description Logics 2020 - [c62]Rasha Faqeh, Christof Fetzer, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Maximilian A. Köhl, Marcel Steinmetz, Christoph Weidenbach:
Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. ISoLA (2) 2020: 416-439 - [c61]Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR 2020: 212-229 - 2019
- [c60]Martin Bromberger, Mathias Fleury
, Simon Schwarz, Christoph Weidenbach:
SPASS-SATT - A CDCL(LA) Solver. CADE 2019: 111-122 - [c59]Alberto Fiori, Christoph Weidenbach:
SCL Clause Learning from Simple Models. CADE 2019: 233-249 - [c58]Andreas Teucke, Marco Voigt, Christoph Weidenbach:
On the Expressivity and Applicability of Model Representation Formalisms. FroCos 2019: 22-39 - [c57]Christoph Weidenbach:
The Challenge of Unifying Semantic and Syntactic Inference Restrictions. ARCADE@CADE 2019: 5-10 - 2017
- [c56]Christoph Weidenbach:
Do Portfolio Solvers Harm? ARCADE@CADE 2017: 76-81 - [c55]Matthias Horbach, Marco Voigt
, Christoph Weidenbach:
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. CADE 2017: 77-94 - [c54]Andreas Teucke, Christoph Weidenbach:
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. CADE 2017: 202-219 - [c53]Jasmin Christian Blanchette
, Mathias Fleury
, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI 2017: 4786-4790 - 2016
- [c52]Noran Azmy, Stephan Merz, Christoph Weidenbach:
A Rigorous Correctness Proof for Pastry. ABZ 2016: 86-101 - [c51]Martin Bromberger, Christoph Weidenbach:
Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. SMT@IJCAR 2016: 15-30 - [c50]Jasmin Christian Blanchette
, Mathias Fleury
, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR 2016: 25-44 - [c49]Ching Hoo Tang, Christoph Weidenbach:
A Dynamic Logic for Configuration. ARQNL@IJCAR 2016: 36-50 - [c48]Andreas Teucke, Christoph Weidenbach:
Ordered Resolution with Straight Dismatching Constraints. PAAR@IJCAR 2016: 95-109 - [c47]Martin Bromberger, Christoph Weidenbach:
Fast Cube Tests for LIA Constraint Solving. IJCAR 2016: 116-132 - [c46]Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski:
Compliance, Functional Safety and Fault Detection by Formal Methods. ISoLA (2) 2016: 626-632 - [c45]Thomas Sturm
, Marco Voigt
, Christoph Weidenbach:
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. LICS 2016: 86-95 - 2015
- [c44]Christoph Weidenbach:
Automated Reasoning Building Blocks. Correct System Design 2015: 172-188 - [c43]Martin Bromberger, Thomas Sturm
, Christoph Weidenbach:
Linear Integer Arithmetic Revisited. CADE 2015: 623-637 - [c42]Gábor Alagi, Christoph Weidenbach:
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. FroCos 2015: 69-84 - [c41]Andreas Teucke, Christoph Weidenbach:
First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. FroCos 2015: 85-100 - [c40]Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, Patrick Wischnewski:
Model-Based Variant Management with v.control. CE 2015: 194-203 - 2013
- [c39]Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm:
Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics 2013: 1-18 - [c38]Thomas Hillenbrand, Christoph Weidenbach:
Superposition for Bounded Domains. Automated Reasoning and Mathematics 2013: 68-100 - [c37]Thomas Hillenbrand, Ruzica Piskac
, Uwe Waldmann, Christoph Weidenbach:
From Search to Computation: Redundancy Criteria and Simplification at Work. Programming Logics 2013: 169-193 - [c36]Noran Azmy, Christoph Weidenbach:
Computing Tiny Clause Normal Forms. CADE 2013: 109-125 - [c35]Deepak Dhungana
, Ching Hoo Tang, Christoph Weidenbach, Patrick Wischnewski:
Automated verification of interactive rule-based configuration systems. ASE 2013: 551-561 - [c34]Manuel Lamotte-Schubert, Christoph Weidenbach:
BDI: A New Decidable First-order Clause Class. LPAR (short papers) 2013: 62-74 - 2012
- [c33]Christoph Weidenbach, Patrick Wischnewski:
Satisfiability Checking and Query Answering for Large Ontologies. PAAR@IJCAR 2012: 163-177 - [c32]Pascal Fontaine, Stephan Merz, Christoph Weidenbach:
Combination of Disjoint Theories: Beyond Decidability. IJCAR 2012: 256-270 - [c31]Martin Suda
, Christoph Weidenbach:
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. IJCAR 2012: 537-543 - [c30]Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP 2012: 345-360 - [c29]Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach:
Automatic Generation of Invariants for Circular Derivations in SUP(LA). LPAR 2012: 197-211 - [c28]Martin Suda
, Christoph Weidenbach:
Labelled Superposition for PLTL. LPAR 2012: 391-405 - 2011
- [c27]Tianxiang Lu, Stephan Merz, Christoph Weidenbach:
Towards Verification of the Pastry Protocol Using TLA + . FMOODS/FORTE 2011: 244-258 - [c26]Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach:
Superposition Modulo Non-linear Arithmetic. FroCoS 2011: 119-134 - 2010
- [c25]Martin Suda
, Christoph Weidenbach, Patrick Wischnewski:
On the Saturation of YAGO. IJCAR 2010: 441-456 - [c24]Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach:
Superposition-Based Analysis of First-Order Probabilistic Timed Automata. LPAR (Yogyakarta) 2010: 302-316 - 2009
- [c23]Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda
, Patrick Wischnewski:
SPASS Version 3.5. CADE 2009: 140-145 - [c22]Matthias Horbach, Christoph Weidenbach:
Decidability Results for Saturation-Based Model Building. CADE 2009: 404-420 - [c21]Matthias Horbach, Christoph Weidenbach:
Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries. CSL 2009: 332-347 - [c20]Ernst Althaus, Evgeny Kruglov, Christoph Weidenbach:
Superposition Modulo Linear Arithmetic SUP(LA). FroCoS 2009: 84-99 - [c19]Manuel Lamotte-Schubert, Christoph Weidenbach:
Analysis of Authorizations in SAP R/3. FTP 2009 - 2008
- [c18]Arnaud Fietzke, Christoph Weidenbach:
Labelled Splitting. IJCAR 2008: 459-474 - [c17]Christoph Weidenbach, Patrick Wischnewski:
Contextual Rewriting in SPASS. PAAR/ESHOL 2008 - [c16]Matthias Horbach, Christoph Weidenbach:
Superposition for Fixed Domains. CSL 2008: 293-307 - 2007
- [c15]Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv:
Labelled Clauses. CADE 2007: 311-327 - [c14]Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic:
System Description: SpassVersion 3.0. CADE 2007: 514-520 - 2002
- [c13]Christoph Weidenbach, Uwe Brahm
, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic:
S PASS Version 2.0. CADE 2002: 275-279 - 2001
- [c12]Bijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach:
First-Order Atom Definitions Extended. LPAR 2001: 309-319 - 1999
- [c11]Christoph Weidenbach:
Towards an Automatic Analysis of Security Protocols in First-Order Logic. CADE 1999: 314-328 - [c10]Christoph Weidenbach:
System Description: Spass Version 1.0.0. CADE 1999: 378-382 - [c9]Ullrich Hustadt, Renate A. Schmidt, Christoph Weidenbach:
MSPASS: Subsumption Testing with SPASS. Description Logics 1999 - 1998
- [c8]Andreas Nonnengart, Georg Rock, Christoph Weidenbach:
On Generating Small Clause Normal Forms. CADE 1998: 397-411 - [c7]Florent Jacquemard, Christoph Meyer, Christoph Weidenbach:
Unification in Extension of Shallow Equational Theories. RTA 1998: 76-90 - 1997
- [c6]Harald Ganzinger, Christoph Meyer, Christoph Weidenbach:
Soft Typing for Ordered Resolution. CADE 1997: 321-335 - 1996
- [c5]Christoph Weidenbach, Bernd Gaede, Georg Rock:
SPASS & FLOTTER Version 0.42. CADE 1996: 141-145 - [c4]Christoph Weidenbach:
Unification in Pseudo-Linear Sort Theories is Decidable. CADE 1996: 343-357 - 1993
- [c3]Christoph Weidenbach:
Extending the Resolution Method with Sorts. IJCAI 1993: 60-65 - 1992
- [c2]Christoph Weidenbach:
A New Sorted Logic. GWAI 1992: 43-54 - 1990
- [c1]Christoph Weidenbach, Hans Jürgen Ohlbach:
A Resolution Calculus with Dynamic Sort Structures and Partial Functions. ECAI 1990: 688-693
Parts in Books or Collections
- 2001
- [p2]Andreas Nonnengart, Christoph Weidenbach:
Computing Small Clause Normal Forms. Handbook of Automated Reasoning 2001: 335-367 - [p1]Christoph Weidenbach:
Combining Superposition, Sorts and Splitting. Handbook of Automated Reasoning 2001: 1965-2013
Editorship
- 2014
- [e2]Stéphane Demri, Deepak Kapur, Christoph Weidenbach:
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Lecture Notes in Computer Science 8562, Springer 2014, ISBN 978-3-319-08586-9 [contents] - 2013
- [e1]Andrei Voronkov, Christoph Weidenbach:
Programming Logics - Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science 7797, Springer 2013, ISBN 978-3-642-37650-4 [contents]
Informal and Other Publications
- 2023
- [i21]Martin Bromberger, Simon Schwarz, Christoph Weidenbach:
SCL(FOL) Revisited. CoRR abs/2302.05954 (2023) - [i20]Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach:
Symbolic Model Construction for Saturated Constrained Horn Clauses. CoRR abs/2305.05064 (2023) - [i19]Martin Bromberger, Chaahat Jain, Christoph Weidenbach:
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CoRR abs/2305.12926 (2023) - 2022
- [i18]Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach:
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR abs/2201.09769 (2022) - [i17]Hendrik Leidinger, Christoph Weidenbach:
SCL(EQ): SCL for First-Order Logic with Equality. CoRR abs/2205.08297 (2022) - [i16]Fajar Haifani, Patrick Koopmann
, Sophie Tourret, Christoph Weidenbach:
Connection-minimal Abduction in EL via Translation to FOL - Technical Report. CoRR abs/2205.08449 (2022) - 2021
- [i15]Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach:
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR abs/2107.03189 (2021) - 2020
- [i14]Alberto Fiori, Christoph Weidenbach:
SCL with Theory Constraints. CoRR abs/2003.04627 (2020) - 2019
- [i13]Andreas Teucke, Marco Voigt, Christoph Weidenbach:
On the Expressivity and Applicability of Model Representation Formalisms. CoRR abs/1905.03651 (2019) - 2017
- [i12]Matthias Horbach, Marco Voigt, Christoph Weidenbach:
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. CoRR abs/1703.01212 (2017) - [i11]Andreas Teucke, Christoph Weidenbach:
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. CoRR abs/1703.02837 (2017) - [i10]Matthias Horbach, Marco Voigt, Christoph Weidenbach:
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. CoRR abs/1705.08792 (2017) - 2015
- [i9]Marco Voigt, Christoph Weidenbach:
Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. CoRR abs/1501.07209 (2015) - [i8]Gábor Alagi, Christoph Weidenbach:
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper). CoRR abs/1502.05501 (2015) - [i7]Martin Bromberger, Thomas Sturm, Christoph Weidenbach:
Linear Integer Arithmetic Revisited. CoRR abs/1503.02948 (2015) - [i6]Andreas Teucke, Christoph Weidenbach:
First-Order Logic Theorem Proving via Counterexample-Guided Abstraction Refinement. CoRR abs/1503.02971 (2015) - [i5]Thomas Sturm, Marco Voigt, Christoph Weidenbach:
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. CoRR abs/1511.08999 (2015) - [i4]Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach:
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5(9): 18-37 (2015) - 2013
- [i3]Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, Patrick Wischnewski:
Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material). CoRR abs/1309.0065 (2013) - [i2]Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach:
Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports 3(10): 1-24 (2013) - 2008
- [i1]Matthias Horbach, Christoph Weidenbach:
Superposition for Fixed Domains. CoRR abs/0809.0922 (2008)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-07-21 22:00 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint