Automated Reasoning

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints
3. Altmetric Badge
   Chapter 2 An SMT Theory of Fixed-Point Arithmetic
4. Altmetric Badge
   Chapter 3 Covered Clauses Are Not Propagation Redundant
5. Altmetric Badge
   Chapter 4 The Resolution of Keller’s Conjecture
6. Altmetric Badge
   Chapter 6 Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
7. Altmetric Badge
   Chapter 7 Solving Bitvectors with MCSAT: Explanations from Bits and Pieces
8. Altmetric Badge
   Chapter 8 Monadic Decomposition in Integer Linear Arithmetic
9. Altmetric Badge
   Chapter 9 Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
10. Altmetric Badge
    Chapter 10 Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
11. Altmetric Badge
    Chapter 12 Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates
12. Altmetric Badge
    Chapter 13 A Decision Procedure for String to Code Point Conversion
13. Altmetric Badge
    Chapter 14 Politeness for the Theory of Algebraic Datatypes
14. Altmetric Badge
    Chapter 15 A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
15. Altmetric Badge
    Chapter 16 A Combinator-Based Superposition Calculus for Higher-Order Logic
16. Altmetric Badge
    Chapter 17 Subsumption Demodulation in First-Order Theorem Proving
17. Altmetric Badge
    Chapter 18 A Comprehensive Framework for Saturation Theorem Proving
18. Altmetric Badge
    Chapter 19 Possible Models Computation and Revision – A Practical Approach
19. Altmetric Badge
    Chapter 20 SGGS Decision Procedures
20. Altmetric Badge
    Chapter 21 Integrating Induction and Coinduction via Closure Operators and Proof Cycles
21. Altmetric Badge
    Chapter 22 Logic-Independent Proof Search in Logical Frameworks
22. Altmetric Badge
    Chapter 23 Layered Clause Selection for Theory Reasoning
23. Altmetric Badge
    Chapter 24 Description Logics with Concrete Domains and General Concept Inclusions Revisited
24. Altmetric Badge
    Chapter 25 A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
25. Altmetric Badge
    Chapter 26 Constructive Hybrid Games
26. Altmetric Badge
    Chapter 26 Constructive Hybrid Games
27. Altmetric Badge
    Chapter 27 Formalizing a Seligman-Style Tableau System for Hybrid Logic
28. Altmetric Badge
    Chapter 28 NP Reasoning in the Monotone $$\mu $$-Calculus
29. Altmetric Badge
    Chapter 29 Soft Subexponentials and Multiplexing
30. Altmetric Badge
    Chapter 30 Mechanised Modal Model Theory