Automated Reasoning

9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings

AvDidier Galmiche,Stephan Schulz

Häftad, Engelska, 2018

Del 10900 i serien Lecture Notes in Computer Science

552 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

This book constitutes the refereed proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, held in Oxford, United Kingdom, in July 2018, as part of the Federated Logic Conference, FLoC 2018.

Produktinformation

Utgivningsdatum:2018-07-01
Mått:155 x 235 x 40 mm
Vikt:1 107 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:724
Förlag:Springer International Publishing AG
ISBN:9783319942049

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Programvaruutveckling inom Data och IT
Artificiell intelligens inom Data och IT

Innehållsförteckning

An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem.- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics.- Superposition for Lambda-Free Higher-Order Logic.- Automated Reasoning about Key Sets.- A Tableaux Calculus for Reducing Proof Size.- FORT 2.0.- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.- The Higher-Order Prover Leo-III.- Well-Founded Unions.- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.- Cubicle-W: Parameterized Model Checking on Weak Memory.- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.- A Why3 framework for reflection proofs and its application to GMP's algorithms.- Infinitely-valued Logic.- Uniform Substitution for Differential Game Logic.- A Logical Framework with Commutative and Non-Commutative Subexponentials.- Exploring Approximations for Floating-Point Arithmetic using UppSAT.- Complexity of Combinations of Qualitative Constraint Satisfaction Problems.- A Generic Framework for Implicate Generation Modulo Theories.- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems.- A New Probabilistic Algorithm for Approximate Model Counting.- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems.- Cops and CoCoWeb: Infrastructure for Conuence Tools.- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing.- Superposition with Datatypes and Codatatypes.- Efficient encodings of first-order Horn formulas in equational logic.- A FOOLish Encoding of the Next State Relations of Imperative Programs.- Constructive Decision via Redundancy-free Proof-Search.- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates.- A Separation Logic with Data: Small Models and Automation.- MaedMax: A Maximal Ordered Completion Tool.- From Syntactic Proofs to Combinatorial Proofs.- A Resolution-Based Calculus for Preferential Logics.- Extended Resolution Simulates DRAT.- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.- Efficient Interpolation for the Theory of Arrays.- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.- Theories as Types.- Datatypes with Shared Selectors.- Enumerating Justifications using Resolution.- A SAT-Based Approach to Learn Explainable Decision Sets.- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.- An abstraction-refinement framework for reasoning with large theories.- Efficient Model Construction for Horn Logic with VLog: System Description.- Focussing, MALL and the polynomial hierarchy.- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.