BibSLEIGH — Proceedings of the 25th International Conference on Automated Deduction

Amy P. Felty, Aart Middeldorp
Proceedings of the 25th International Conference on Automated Deduction
CADE, 2015.

TEST

@proceedings{CADE-2015,
	address       = "Berlin, Germany",
	doi           = "10.1007/978-3-319-21401-6",
	editor        = "Amy P. Felty and Aart Middeldorp",
	isbn          = "978-3-319-21400-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 25th International Conference on Automated Deduction}",
	volume        = 9195,
	year          = 2015,
}

Contents (42 items)

CADE-2015-Plaisted #automation #deduction #first-order: History and Prospects for First-Order Automated Deduction (DAP), pp. 3–28.
CADE-2015-Martin #lessons learnt: Stumbling Around in the Dark: Lessons from Everyday Mathematics (UM), pp. 29–51.
CADE-2015-FurbachPS #automation #reasoning: Automated Reasoning in the Wild (UF, BP, CS), pp. 55–72.
CADE-2015-AlamaOZ #automation #concept: Automating Leibniz’s Theory of Concepts (JA, PEO, ENZ), pp. 73–97.
CADE-2015-AotoHN0Z #confluence #contest: Confluence Competition 2015 (TA, NH, JN, NN, HZ), pp. 101–104.
CADE-2015-GieslMRTW #contest #termination: Termination Competition (termCOMP 2015) (JG, FM, AR, RT, JW), pp. 105–108.
CADE-2015-SakaiOO #confluence: Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent (MS, MO, MO), pp. 111–126.
CADE-2015-ShintaniH #confluence #linear #named #term rewriting: CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems (KS, NH), pp. 127–136.
CADE-2015-JacquemardKS #bottom-up #constraints #term rewriting: Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies (FJ, YK, MS), pp. 137–151.
CADE-2015-SatoW #dependence #encoding: Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion (HS, SW), pp. 152–162.
CADE-2015-IborraNVY #dependence #problem #termination: Reducing Relative Termination to Dependency Pair Problems (JI, NN, GV, AY), pp. 163–178.
CADE-2015-Passmore #algebra #decidability #integer: Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers (GOP), pp. 181–196.
CADE-2015-ReynoldsB #data type #smt: A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.
CADE-2015-David #satisfiability: Deciding ATL* Satisfiability by Tableaux (AD), pp. 214–228.
CADE-2015-Paulson #automaton #finite #formal method #set #using: A Formalisation of Finite Automata Using Hereditarily Finite Sets (LCP), pp. 231–245.
CADE-2015-GransdenWR #automaton #named #proving #using: SEPIA: Search for Proofs Using Inferred Automata (TG, NW, RR), pp. 246–255.
CADE-2015-MaricJM #correctness #higher-order #proving #using: Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
CADE-2015-PientkaC #induction #programming #proving: Inductive Beluga: Programming Proofs (BP, AC), pp. 272–281.
CADE-2015-Baumgartner #named #proving #theorem proving: SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
CADE-2015-Ji #deduction #model checking: CTL Model Checking in Deduction Modulo (KJ), pp. 295–310.
CADE-2015-EchenimPT #equation #generative #logic #quantifier: Quantifier-Free Equational Logic and Prime Implicate Generation (ME, NP, ST), pp. 311–325.
CADE-2015-KissingerZ #diagrams #named #proving #reasoning: Quantomatic: A Proof Assistant for Diagrammatic Reasoning (AK, VZ), pp. 326–336.
CADE-2015-RegerTV #proving: Cooperating Proof Attempts (GR, DT, AV), pp. 339–355.
CADE-2015-GorznyP #first-order #proving #towards: Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (JG, BWP), pp. 356–366.
CADE-2015-BaumgartnerBW #named #proving #theorem proving: Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.
CADE-2015-MouraKADR #agile #proving #theorem proving: The Lean Theorem Prover (LMdM, SK, JA, FvD, JvR), pp. 378–388.
CADE-2015-KaliszykSUV: System Description: E.T. 0.1 (CK, SS, JU, JV), pp. 389–398.
CADE-2015-RegerSV #game studies: Playing with AVATAR (GR, MS, AV), pp. 399–415.
CADE-2015-ChocronFR #revisited: A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited (PC, PF, CR), pp. 419–433.
CADE-2015-SaghafiDD: Exploring Theories with a Model-Finding Assistant (SS, RD, DJD), pp. 434–449.
CADE-2015-DSilvaU #abstract interpretation #automation #deduction: Abstract Interpretation as Automated Deduction (VD, CU), pp. 450–464.
CADE-2015-Platzer #calculus #difference #logic: A Uniform Substitution Calculus for Differential Dynamic Logic (AP), pp. 467–481.
CADE-2015-TiwariGD #synthesis #using: Program Synthesis Using Dual Interpretation (AT, AG, BD), pp. 482–497.
CADE-2015-HouGT #automation #logic #proving #theorem proving: Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
CADE-2015-DinBH #concurrent #deduction #modelling #named #verification: KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS (CCD, RB, RH), pp. 517–526.
CADE-2015-FultonMQVP #axiom #hybrid #proving #theorem proving: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (NF, SM, JDQ, MV, AP), pp. 527–538.
CADE-2015-BalbianiB #composition #logic #parallel: Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition (PB, JB), pp. 539–554.
CADE-2015-Libal #higher-order #unification: Regular Patterns in Second-Order Unification (TL), pp. 557–571.
CADE-2015-BackemanR #bound #proving #theorem proving: Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
CADE-2015-HeuleHW #proving #symmetry: Expressing Symmetry Breaking in DRAT Proofs (MH, WAHJ, NW), pp. 591–606.
CADE-2015-ZulkoskiGC #algebra #named #satisfiability: MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (EZ, VG, KC), pp. 607–622.
CADE-2015-Bromberger0W #integer #linear #revisited: Linear Integer Arithmetic Revisited (MB, TS, CW), pp. 623–637.

Amy P. Felty, Aart MiddeldorpProceedings of the 25th International Conference on Automated DeductionCADE, 2015.

Contents (42 items)

Amy P. Felty, Aart Middeldorp
Proceedings of the 25th International Conference on Automated Deduction
CADE, 2015.