Automated reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings. Part I

Automated reasoning : Part I / 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings. Nicolas Peltier, Viorica Sofronie-Stokkermans (eds.).

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 Aut...

Full description

Saved in:
Bibliographic Details
Corporate Author: IJCAR (Conference) Online)
Other Authors: Peltier, Nicolas, Sofronie-Stokkermans, Viorica
Format: eBook
Language:English
Published: Cham : Springer, 2020.
Series:Lecture notes in computer science ; 12166.
Lecture notes in computer science. Lecture notes in artificial intelligence.
LNCS sublibrary. Artificial intelligence.
Subjects:
Automatic theorem proving > Congresses.
Computer logic > Congresses.
Artificial intelligence.
Computer programming > software development.
Software Engineering.
Programming & scripting languages: general.
Mathematical theory of computation.
Computers > Intelligence (AI) & Semantics.
Computers > Programming > General.
Computers > Software Development & Engineering > General.
Computers > Programming Languages > General.
Mathematics > Logic.
Automatic theorem proving
Computer logic
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
Online Access:Click for online access
Table of Contents:
  • 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 Kellers 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.

Similar Items