| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910495194703321 |
|
|
Titolo |
Frontiers of Combining Systems : 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021, Proceedings / / edited by Boris Konev, Giles Reger |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2021.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (314 pages) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence, , 2945-9141 ; ; 12941 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Artificial intelligence |
Software engineering |
Computer engineering |
Computer networks |
Computer science |
Machine theory |
Artificial Intelligence |
Software Engineering |
Computer Engineering and Networks |
Computer Science Logic and Foundations of Programming |
Formal Languages and Automata Theory |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Calculi and Unification -- A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic -- Non-Disjoint Combined Unification and Closure by Equational Paramodulation -- Symbol Elimination and Applications to Parametric Entailment Problems -- On the copy complexity of width 3 Horn constraint systems -- Description Logics Restricted Unification in the Description Logic FL0 -- Combining Event Calculus and Description Logic Reasoning via Logic Programming -- Semantic Forgetting in Expressive Description Logics -- Interactive Theorem Proving Improving Automation for Higher-order Proof Steps -- JEFL: Joint Embedding of Formal Proof Libraries -- Machine Learning Fast and Slow Enigmas and Parental Guidance -- Vampire With a Brain |
|
|
|
|
|
|
|
|
|
|
|
Is a Good ITP Hammer -- Satisfiability Modulo Theories Optimization Modulo Non-Linear Arithmetic via Incremental Linearization -- Quantifier Simplification by Unification in SMT -- Verification Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems -- Formal Analysis of Symbolic Authenticity -- Formal Verification of a Java Component Using the RESOLVE Framework. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the refereed proceedings of the 13th International Symposium on Frontiers of Combining Systems, FroCoS 2021, held in Birmingham, UK, in September 2021. |
|
|
|
|
|
|
|
| |