Pascal Fontaine
Proceddings of the 27th International Conference on Automated Deduction
CADE, 2019.

@proceedings{CADE-2019,
	doi           = "10.1007/978-3-030-29436-6",
	editor        = "Pascal Fontaine",
	isbn          = "['978-3-030-29435-9', '978-3-030-29436-6']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceddings of the 27th International Conference on Automated Deduction}",
	volume        = 11716,
	year          = 2019,
}

Contents (34 items)

CADE-2019-AnantharamanHNR #equation #unification #word

Unification Modulo Lists with Reverse Relation with Certain Word Equations (SA, PH, PN, MR), pp. 1–17.

CADE-2019-MeloO #finite #on the

On the Width of Regular Classes of Finite Structures (AAdM, MdOO), pp. 18–34.

CADE-2019-BarbosaROTB #higher-order #logic #smt

Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.

CADE-2019-BentkampBTVW

Superposition with Lambdas (AB, JB, ST, PV, UW), pp. 55–73.

CADE-2019-BhayatR #combinator #strict #unification

Restricted Combinatory Unification (AB, GR), pp. 74–93.

CADE-2019-BohrerFP #difference #logic #named

dLι: Definite Descriptions in Differential Dynamic Logic (BB, MF, AP), pp. 94–110.

CADE-2019-BrombergerFSW

SPASS-SATT - A CDCL(LA) Solver (MB, MF, SS, CW), pp. 111–122.

CADE-2019-BrownGKSU #challenge #named

GRUNGE: A Grand Unified ATP Challenge (CEB, TG, CK, GS, JU), pp. 123–141.

CADE-2019-CalvaneseGGMR

Model Completeness, Covers and Superposition (DC, SG, AG, MM, AR), pp. 142–160.

CADE-2019-CassanoFHAC #calculus #logic

A Tableaux Calculus for Default Intuitionistic Logic (VC, RF, GH, CA, PFC), pp. 161–177.

CADE-2019-ChenWAZKZ #learning #named

NIL: Learning Nonlinear Interpolants (MC, JW0, JA, BZ, DK, NZ), pp. 178–196.

CADE-2019-ChvalovskyJ0U #named #performance

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E (KC, JJ, MS0, JU), pp. 197–215.

CADE-2019-CordwellP #hybrid #physics #towards

Towards Physical Hybrid Systems (KC, AP), pp. 216–232.

CADE-2019-FioriW #learning #modelling

SCL Clause Learning from Simple Models (AF, CW), pp. 233–249.

CADE-2019-FurbachKS #axiom #word

Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection (UF, TK, CS), pp. 250–268.

CADE-2019-GieslGH #constant #probability #source code

Computing Expected Runtimes for Constant Probability Programs (JG, PG, MH), pp. 269–286.

CADE-2019-GutierrezL #automation #generative #logic #modelling

Automatic Generation of Logical Models with AGES (RG, SL), pp. 287–299.

CADE-2019-HavlenaHLV #automaton #lazy evaluation

Automata Terms in a Lazy WSkS Decision Procedure (VH, LH, OL, TV), pp. 300–318.

CADE-2019-HirokawaNOO #analysis #confluence #revisited

Confluence by Critical Pair Analysis Revisited (NH, JN, VvO, MO), pp. 319–336.

CADE-2019-KohlM #proving

Composing Proof Terms (CK, AM), pp. 337–353.

CADE-2019-LiT #automation #protocol #proving #security #theorem proving #verification

Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (DLL, AT), pp. 354–365.

CADE-2019-NiemetzPRZBT #independence #proving #smt #towards

Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.

CADE-2019-PeuterS #invariant #on the #parametricity #synthesis

On Invariant Synthesis for Parametric Systems (DP, VSS), pp. 385–405.

CADE-2019-Plaisted #calculus

The Aspect Calculus (DAP), pp. 406–424.

CADE-2019-Platzer

Uniform Substitution at One Fell Swoop (AP), pp. 425–441.

CADE-2019-0001T #theorem

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems (AP0, DT), pp. 442–461.

CADE-2019-RawsonR

Old or Heavy? Decaying Gracefully with Age/Weight Shapes (MR, GR), pp. 462–476.

CADE-2019-RegerV #induction #proving

Induction in Saturation-Based Proof Search (GR, AV), pp. 477–494.

CADE-2019-0001CV #performance

Faster, Higher, Stronger: E 2.3 (SS0, SC, PV), pp. 495–507.

CADE-2019-SternagelW #equation #order #reasoning

Certified Equational Reasoning via Ordered Completion (CS, SW), pp. 508–525.

CADE-2019-SutcliffeP #logic #named

JGXYZ: An ATP System for Gap and Glut Logics (GS, FJP), pp. 526–537.

CADE-2019-Tammet #knowledge base #named #reasoning #scalability

GKC: A Reasoning System for Large Knowledge Bases (TT), pp. 538–549.

CADE-2019-TrentinS #float #formal method #optimisation

Optimization Modulo the Theory of Floating-Point Numbers (PT, RS), pp. 550–567.

CADE-2019-ZhaoS #automation #logic #strict

FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions (YZ, RAS), pp. 568–579.