Automated Reasoning 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II /
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...
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Language: | English |
| Published: |
Cham :
Springer International Publishing : Imprint: Springer,
2020.
|
| Edition: | 1st ed. 2020. |
| Series: | Lecture Notes in Artificial Intelligence ;
12167 |
| Subjects: | |
| Online Access: | https://doi.org/10.1007/978-3-030-51054-1 |
Table of Contents:
- Interactive Theorem Proving/ HOL
- Competing inheritance paths in dependent type theory: a case study in functional analysis
- A Lean tactic for normalising ring expressions with exponents (short paper)
- Practical proof search for Coq by type inhabitation
- Quotients of Bounded Natural Functors
- Trakhtenbrot’s Theorem in Coq
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Validating Mathematical Structures
- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
- Formalizations
- Formalizing the Face Lattice of Polyhedra
- Algebraically Closed Fields in Isabelle/HOL
- Formalization of Forcing in Isabelle/ZF
- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL
- Formal Proof of the Group Law for Edwards Elliptic Curves
- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation
- Verification
- Verified Approximation Algorithms
- Efficient Verified Implementation of Introsort and Pdqsort
- A Fast Verified Liveness Analysis in SSA form
- Verification of Closest Pair of Points Algorithms
- Reasoning Systems and Tools
- A Polymorphic Vampire (short paper)
- N-PAT: A Nested Model-Checker (system description)
- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
- Implementing superposition in iProver (system description)
- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
- Make E Smart Again
- Automatically Proving and Disproving Feasibility Conditions
- µ-term: Verify Termination Properties Automatically (system description)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
- The Imandra Automated Reasoning System (system description)
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)
- Sequoia: a playground for logicians (system description)
- Prolog Technology Reinforcement Learning Prover (system description).