Questo prodotto usufruisce delle SPEDIZIONI GRATIS
selezionando l'opzione Corriere Veloce in fase di ordine.
Pagabile anche con Carta della cultura giovani e del merito, 18App Bonus Cultura e Carta del Docente
This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods).
The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics:
Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics
Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools
*The conference was held virtually due to the COVID-19 pandemic.
Chapter ‘Constructive Hybrid Games’ is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.
Invited Paper.- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints.- SAT; SMT and QBF.- An SMT Theory of Fixed-Point Arithmetic.- Covered Clauses Are Not Propagation Redundant.- The Resolution of Keller’s Conjecture.- How QBF Expansion Makes Strategy Extraction Hard.- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates.- Solving bit-vectors with MCSAT: explanations from bits and pieces.- Monadic Decomposition in Integer Linear Arithmetic.- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.- Decision Procedures and Combination of Theories.- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols.- Combined Covers and Beth Definability.- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates.- A Decision Procedure for String to Code Point Conversion.- Politeness for The Theory of Algebraic Datatypes.- Superposition.- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations.- A Combinator-Based Superposition Calculus for Higher-Order Logic.- Subsumption Demodulation in First-Order Theorem Proving.- A Comprehensive Framework for Saturation Theorem Proving.- Proof Procedures.- Possible Models Computation and Revision - A Practical Approach.- SGGS Decision Procedures.- Integrating Induction and Coinduction via Closure Operators and Proof Cycles.- Logic-Independent Proof Search in Logical Frameworks (short paper).- Layered Clause Selection for Theory Reasoning (short paper).- Non Classical Logics.- Description Logics with Concrete Domains and General Concept Inclusions Revisited.- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.- Constructive Hybrid Games.- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper).- NP Reasoning in the Monotone µ-Calculus.- Soft subexponentials and multiplexing.- Mechanised Modal Model Theory.
Il sito utilizza cookie ed altri strumenti di tracciamento che raccolgono informazioni dal dispositivo dell’utente. Oltre ai cookie tecnici ed analitici aggregati, strettamente necessari per il funzionamento di questo sito web, previo consenso dell’utente possono essere installati cookie di profilazione e marketing e cookie dei social media. Cliccando su “Accetto tutti i cookie” saranno attivate tutte le categorie di cookie. Per accettare solo deterninate categorie di cookie, cliccare invece su “Impostazioni cookie”. Chiudendo il banner o continuando a navigare saranno installati solo cookie tecnici. Per maggiori dettagli, consultare la Cookie Policy.