BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × Denmark
1 × Japan
1 × Portugal
2 × Australia
2 × Italy
2 × United Kingdom
3 × Germany
3 × USA
Collaborated with:
M.Horbach M.Bromberger M.Suda P.Wischnewski A.Fietzke G.Rock C.Meyer M.Fleury N.Azmy A.Teucke A.Fiori T.Hillenbrand D.Topic T.Sturm P.Fontaine S.Merz A.Nonnengart F.Jacquemard H.Ganzinger B.Gaede J.C.Blanchette M.Voigt D.Dhungana C.H.Tang T.Lev-Ami T.W.Reps M.Sagiv S.Schwarz R.A.Schmidt R.Rusev D.Dimova R.Kumar U.Brahm E.Keen C.Theobalt
Talks about:
version (5) spass (5) decid (5) linear (4) claus (4) theori (3) system (3) order (3) model (3) label (3)

Person: Christoph Weidenbach

DBLP DBLP: Weidenbach:Christoph

Facilitated 1 volumes:

IJCAR 2014Ed

Contributed to:

CADE 20152015
ASE 20132013
CADE 20132013
IJCAR 20122012
IJCAR 20102010
CADE 20092009
CSL 20092009
CSL 20082008
IJCAR 20082008
CADE 20072007
CADE 20022002
CADE 19991999
CADE 19981998
RTA 19981998
CADE 19971997
CADE 19961996
IJCAR 20162016
CADE 20172017
CADE 20192019

Wrote 27 papers:

CADE-2015-Bromberger0W #integer #linear #revisited
Linear Integer Arithmetic Revisited (MB, TS, CW), pp. 623–637.
ASE-2013-DhunganaTWW #automation #interactive #rule-based #verification
Automated verification of interactive rule-based configuration systems (DD, CHT, CW, PW), pp. 551–561.
CADE-2013-AzmyW #normalisation
Computing Tiny Clause Normal Forms (NA, CW), pp. 109–125.
IJCAR-2012-FontaineMW #decidability
Combination of Disjoint Theories: Beyond Decidability (PF, SM, CW), pp. 256–270.
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance (MS, CW), pp. 537–543.
IJCAR-2010-SudaWW #on the
On the Saturation of YAGO (MS, CW, PW), pp. 441–456.
CADE-2009-HorbachW #decidability
Decidability Results for Saturation-Based Model Building (MH, CW), pp. 404–420.
SPASS Version 3.5 (CW, DD, AF, RK, MS, PW), pp. 140–145.
CSL-2009-HorbachW #induction #query
Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries (MH, CW), pp. 332–347.
Superposition for Fixed Domains (MH, CW), pp. 293–307.
Labelled Splitting (AF, CW), pp. 459–474.
Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.
System Description: SpassVersion 3.0 (CW, RAS, TH, RR, DT), pp. 514–520.
S PASS Version 2.0 (CW, UB, TH, EK, CT, DT), pp. 275–279.
CADE-1999-Weidenbach #analysis #automation #first-order #logic #protocol #security #towards
Towards an Automatic Analysis of Security Protocols in First-Order Logic (CW), pp. 314–328.
System Description: Spass Version 1.0.0 (CW), pp. 378–382.
CADE-1998-NonnengartRW #generative #normalisation #on the
On Generating Small Clause Normal Forms (AN, GR, CW), pp. 397–411.
RTA-1998-JacquemardMW #equation #unification
Unification in Extension of Shallow Equational Theories (FJ, CM, CW), pp. 76–90.
CADE-1997-GanzingerMW #order #type system
Soft Typing for Ordered Resolution (HG, CM, CW), pp. 321–335.
CADE-1996-Weidenbach #decidability #pseudo #unification
Unification in Pseudo-Linear Sort Theories is Decidable (CW), pp. 343–357.
SPASS & FLOTTER Version 0.42 (CW, BG, GR), pp. 141–145.
IJCAR-2016-BlanchetteFW #framework #satisfiability
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (JCB, MF, CW), pp. 25–44.
IJCAR-2016-BrombergerW #constraints #performance #testing #theorem proving
Fast Cube Tests for LIA Constraint Solving (MB, CW), pp. 116–132.
CADE-2017-HorbachVW #integer #linear #on the
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic (MH, MV, CW), pp. 77–94.
CADE-2017-TeuckeW #constraints #decidability #first-order #linear #monad
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints (AT, CW), pp. 202–219.
SPASS-SATT - A CDCL(LA) Solver (MB, MF, SS, CW), pp. 111–122.
CADE-2019-FioriW #learning #modelling
SCL Clause Learning from Simple Models (AF, CW), pp. 233–249.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.