View: session overviewtalk overview
10:30 | Certified Equational Reasoning via Ordered Completion PRESENTER: Sarah Winkler ABSTRACT. On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes implementations inherently error prone. As a remedy, we provide a formally verified certifier for ordered completion based techniques. This certifier is code generated from an accompanying Isabelle/HOL formalization of ordered rewriting and ordered completion incorporating an advanced ground joinability criterion. It allows us to rigorously validate generated proof certificates from several domains: ordered completion, satisfiability in equational logic, and confluence of conditional term rewriting. |
11:00 | Unification modulo Lists with Reverse - Relation with Certain Word Equations PRESENTER: Peter Hibbs ABSTRACT. Decision procedures for various list theories has been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists. |
11:30 | Confluence by Critical Pair Analysis Revisited ABSTRACT. We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating. |
12:00 | Composing Proof Terms PRESENTER: Christina Kohl ABSTRACT. Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for for manipulating proof terms. |