PROGRAM
Days: Wednesday, July 1st Thursday, July 2nd Friday, July 3rd Saturday, July 4th
Wednesday, July 1st
View this program: with abstractssession overviewtalk overview
11:30-12:30 Session 1: FSCD-IJCAR Invited Speaker: R. Thiemann (all times are in CEST timezone - UTC+2)
FSCD-IJCAR Invited Speaker: R. Thiemann
13:00-15:00 Session 2A: Superposition and Saturation-Based Theorem Proving
Chair:
| 13:00 | Subsumption Demodulation in First-Order Theorem Proving (abstract) |
| 13:30 | A Knuth-Bendix-Like Ordering for Orienting Combinator Equations (abstract) |
| 14:00 | A Comprehensive Framework for Saturation Theorem Proving (abstract) |
| 14:30 | A Combinator-Based Superposition Calculus for Higher-Order Logic (abstract) |
13:00-15:00 Session 2B: Interactive Theorem Proving
Chair:
| 13:00 | Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis (abstract) |
| 13:30 | Quotients of Bounded Natural Functors (abstract) |
| 14:00 | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (abstract) |
| 14:30 | Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (abstract) |
15:15-16:15 Session 3: Invited IJCAR-FSCD Talk: J. Harrison
Chair:
| 15:15 | Adventures in Verifying Arithmetic (abstract) |
16:45-17:45 Session 4A: Machine Learning and Theory Reasoning
Chair:
| 16:45 | ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) (abstract) |
| 17:00 | Prolog Technology Reinforcement Learning Prover (system description) (abstract) |
| 17:15 | Layered Clause Selection for Theory Reasoning (short paper) (abstract) |
| 17:30 | Make E Smart Again (short paper) (abstract) |
16:45-18:00 Session 4B: Formalizing Non Classical Logics
Chair:
| 16:45 | Mechanised Modal Model Theory (abstract) |
| 17:15 | Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) (abstract) |
| 17:30 | A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic (abstract) |
Thursday, July 2nd
View this program: with abstractssession overviewtalk overview
13:00-15:00 Session 6A: SAT, SMT and QBF
Chair:
| 13:00 | The Resolution of Keller's Conjecture (abstract) |
| 13:30 | How QBF Expansion Makes Strategy Extraction Hard (abstract) |
| 14:00 | Covered Clauses Are Not Propagation Redundant (abstract) |
| 14:30 | Solving bit-vectors with MCSAT: explanations from bits and pieces (abstract) |
13:00-15:00 Session 6B: Isabelle
Chair:
| 13:00 | Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL (abstract) |
| 13:30 | Algebraically Closed Fields in Isabelle/HOL (abstract) |
| 14:00 | Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation (abstract) |
| 14:30 | Formalization of Forcing in Isabelle/ZF (abstract) |
15:15-16:15 Session 7: Invited Talk: E. Pimentel
Chair:
| 15:15 | Focusing, axioms and synthetic inference rules (extended abstract) (abstract) |
16:30-18:30 Session 8A: Non Classical Logics
Chair:
| 16:30 | Soft subexponentials and multiplexing (abstract) |
| 17:00 | Description Logics with Concrete Domains and General Concept Inclusions Revisited (abstract) |
| 17:30 | Constructive Hybrid Games (abstract) |
| 18:00 | NP Reasoning in the Monotone mu-Calculus (abstract) |
16:30-18:00 Session 8B: Reasoning Systems, Tactics and Tools
Chair:
| 16:30 | A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) (abstract) |
| 16:45 | Sequoia: a playground for logicians (system description) (abstract) |
| 17:00 | HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) (abstract) |
| 17:15 | Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) (abstract) |
| 17:30 | A Lean tactic for normalising ring expressions with exponents (short paper) (abstract) |
| 17:45 | Logic-Independent Proof Search in Logical Frameworks (short paper) (abstract) |
18:30-20:00 Session 9: Business Meetings (IJCAR, FROCOS, TABLEAUX, CADE)
Report of IJCAR 2020 PC co-chairs (N. Peltier)
Best Paper Award (V. Sofronie-Stokkermans)
Report of IJCAR 2020 Conference Chair (K. Chaudhuri)
Information regarding CADE 2021, FroCoS 2021, Tableaux 2021, and IJCAR 2022
Chairs: Franz Baader, Jens Otten, Christoph Weidenbach
Friday, July 3rd
View this program: with abstractssession overviewtalk overview
13:00-15:00 Session 10A: Proof Procedures, Decision Procedures and Combination of Theories
Chair:
| 13:00 | Politeness for The Theory of Algebraic Datatypes (abstract) |
| 13:30 | Combined Covers and Beth Definability (abstract) |
| 14:00 | Possible Models Computation and Revision - A Practical Approach (abstract) |
| 14:30 | SGGS Decision Procedures (abstract) |
13:00-15:00 Session 10B: Coq
Chair:
| 13:00 | Practical proof search for Coq by type inhabitation (abstract) |
| 13:30 | Formalizing the Face Lattice of Polyhedra (abstract) |
| 14:00 | Trakhtenbrot's Theorem in Coq (abstract) |
| 14:30 | Deep Generation of Coq Lemma Names Using Elaborated Terms (abstract) |
15:15-16:15 Session 11: Invited Talk: R. Piskac
Chair:
| 15:15 | Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints (abstract) |
16:30-17:30 Session 12A: Formalization
Chair:
| 16:30 | Validating Mathematical Structures (abstract) |
| 17:00 | Formal Proof of the Group Law for Edwards Elliptic Curves (abstract) |
16:30-18:30 Session 12B: Decision Procedures, Rewriting and Model Checking
Chair:
| 16:30 | Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols (abstract) |
| 17:00 | A Decision Procedure for String to Code Point Conversion (abstract) |
| 17:30 | mu-term: Verify Termination Properties Automatically (system description) (abstract) |
| 17:45 | Automatically Proving and Disproving Feasibility Conditions (abstract) |
| 18:15 | N-PAT: A Nested Model-Checker (system description) (abstract) |
Saturday, July 4th
View this program: with abstractssession overviewtalk overview
13:00-15:00 Session 13A: Satisfiability Modulo Theories
Chair:
| 13:00 | Monadic Decomposition in Integer Linear Arithmetic (abstract) |
| 13:30 | An SMT Theory of Fixed-Point Arithmetic (abstract) |
| 14:00 | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis (abstract) |
| 14:30 | Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates (abstract) |
13:00-15:00 Session 13B: Verification
Chair:
| 13:00 | Efficient Verified Implementation of Introsort and Pdqsort (abstract) |
| 13:30 | A Fast Verified Liveness Analysis in SSA form (abstract) |
| 14:00 | Verified Approximation Algorithms (abstract) |
| 14:30 | Verification of Closest Pair of Points Algorithms (abstract) |
15:15-16:15 Session 14: Invited Talk: C.Barrett
Chair:
| 15:15 | Domain-Specific Reasoning with Satisfiability Modulo Theories (abstract) |
16:30-18:00 Session 15A: Results of Competitions, Reasoning Systems
Chair:
| 16:30 | Termination Competition (abstract) |
| 16:45 | The CADE ATP System Competition Presentation (abstract) |
| 17:00 | A Polymorphic Vampire (short paper) (abstract) |
| 17:15 | Implementing superposition in iProver (system description) (abstract) |
| 17:30 | Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) (abstract) |
| 17:45 | The Imandra Automated Reasoning System (system description) (abstract) |
16:30-17:30 Session 15B: Induction, co-Induction and Infinity Axioms
Chair:
| 16:30 | Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates (abstract) |
| 17:00 | Integrating Induction and Coinduction via Closure Operators and Proof Cycles (abstract) |