Automated deduction -- CADE 27 : 27th international conference on automated deduction, Natal, Brazil, August 27-30, 2019 : proceedings /: 27th international conference on automated deduction, Natal, Brazil, August 27-30, 2019 : proceedings. ([2019])

• Record Type: Book
• Further Information: Note: Pascal Fontaine (ed.).
• Editors: (Professor of Computer Science), Fontaine, Pascal
• Other Names: International Conference on Automated Deduction, 27th
• Contents: Automated Reasoning for Security Protocols -- Computer Deduction and (Formal) Proofs in Mathematics -- From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT -- The CADE-27 ATP System Competition -- CASC-27 -- Unification modulo Lists with Reverse -- Relation with Certain Word Equations -- On the Width of Regular Classes of Finite Structures -- Extending SMT solvers to Higher-Order Logic -- Superposition with Lambdas -- Restricted Combinatory Unification -- dLi: Definite Descriptions in Differential Dynamic Logic -- SPASS-SATT { A CDCL(LA) Solver -- GRUNGE: A Grand Unified ATP Challenge -- Model Completeness, Covers and Superposition -- A Tableaux Calculus for Default Intuitionistic Logic -- NIL: Learning Nonlinear Interpolants -- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E -- Towards Physical Hybrid Systems -- SCL -- Clause Learning from Simple Models -- Names are not just Sound and Smoke: Word Embeddings for Axiom Selection -- Computing Expected Runtimes for Constant Probability Programs -- Automatic Generation of Logical Models with AGES -- Automata Terms in a Lazy WSkS Decision Procedure -- Confluence by Critical Pair Analysis Revisited -- Composing Proof Terms -- Combining ProVerif and Automated Theorem Provers for Security Protocol Verification -- Towards Bit-Width-Independent Proofs in SMT Solvers -- On Invariant Synthesis for Parametric Systems -- The Aspect Calculus -- Uniform Substitution At One Fell Swoop -- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems -- Old or Heavy? Decaying Gracefully with Age/Weight Shapes -- Induction in Saturation-Based Proof Search -- Faster, Higher, Stronger: E 2.3 -- Certified Equational Reasoning via Ordered Completion -- JGXYZ -- An ATP System for Gap and Glut Logics -- GKC: a Reasoning System for Large Knowledge Bases -- Optimization Modulo the Theory of Floating-Point Numbers -- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions.
• Publisher Details: Cham : Springer
• Publication Date: 2019
• Copyright Date: 2019
• Extent: 1 online resource, illustrations (some color)
• Subjects: 511.3/6028563; Automatic theorem proving -- Congresses; Logic, Symbolic and mathematical -- Congresses; Théorèmes -- Démonstration automatique -- Congrès; Logique symbolique et mathématique -- Congrès; Automatic theorem proving; Logic, Symbolic and mathematical; Conference papers and proceedings; Conference papers and proceedings; Actes de congrès
• Languages: English
• ISBNs: 9783030294366; 3030294366; 3030294358; 9783030294359; 9783030294373; 3030294374
• Notes: Note: Includes bibliographical references and index.; Note: Online resource; title from PDF title page (SpringerLink, viewed September 11, 2019).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.