IsaFoR/CeTA - An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions

Versions

To check the version, just invoke CeTA with --version or without arguments (for version v2.28 or older).

Version 3.2 (28 June 2024)
- feasibility proofs
- improved error messages for rejected non-commutation proofs
- swapping of TRSs is possible in non-commutation proofs
Version 3.1 (14 June 2024)
- switch to Isabelle 2024
- support for split-if transformation
- formalization of narrowing and multiset-narrowing
Version 3.0.1 (16 November 2023)
- minor fixes in cpf3HTML and in CPF 2-to-3 converter
Version 3.0 (13 November 2023)
- switch to CPF 3 (quick overview: README; full archive with converter: cpf3.tgz; certificates of competitions in CPF 3 format)
- WPO, CoWPO and polynomial interpretations over the negative integers can used as co-rewrite pairs for infeasibility
- monotone semantic path order
- generalized WPO
- non-joinability of terms can be shown if only finitely many terms are reachable
Version 2.46 (14 September 2023)
- faster rewrite engine
- compositional parallel critical pairs systems certificates may contain joining sequences
- switch to Isabelle 2023
Version 2.45.1 (29 August 2023)
- intermediate version of CeTA for CoCo full run
- discrimination pairs for non-joinability are now tested in both directions
Version 2.45 (20 June 2023)
- improved efficiency of RPO implementation from cubic to quadratic (for fixed signature)
- improved efficiency of WPO implementation from exponential to polynomial
Version 2.44 (10 March 2023)
- almost development closed criterion for commutation
- parallel critical pair closed as criterion for confluence and commutation
- rule labeleling with parallel critical pairs for confluence and commutation
- compositional techniques for confluence and commutation based on parallel critical pairs
- infeasibility proofs are supported as top-level proof obligations
Version 2.43 (27 October 2022)
- switch to Isabelle 2022
- decision procedure for (innermost-)right ground termination
- improved bound for solving linear integer arithmetic constraints
- support of commutation: non-joins and almost parallel closed systems
Version 2.42 (14 June 2022)
- development-closed as confluence criterion
- improved efficiency of parser
Version 2.41 (15 December 2021)
- switch to Isabelle 2021-1
Version 2.40 (17 June 2021)
- generalization of the weighted path order that permits multiset comparisons
- several extensions w.r.t. LLVM termination proving
- switch to Isabelle 2021
Version 2.39 (29 April 2020)
- integration of the weighted path order (WPO)
- argument filters in combination with arbitrary reduction pairs
- max-polynomial interpretations
- switch to Isabelle 2020
Version 2.38 (19 December 2019)
- the internal theory solver now supports full linear integer arithmetic, instead of approximating validity via linear rational arithmetic
Version 2.37 (20 June 2019)
- switch to Isabelle 2019
Version 2.36 (1 April 2019)
- certification of ordered completion for infeasibility
Version 2.35 (26 November 2018)
- Support for ACKBO.
- Use String.literal for error message to have smaller and more readable Haskell code.
Version 2.34 (20 August 2018)
- improved session structure of theories: logical and build sessions
- Isabelle's char type is no longer mapped to Haskell's built-in char type ⟶ decrease in efficiency
- switch to Isabelle 2018
Version 2.33 (25 May 2018)
- certification of ordered completion
- no algebraic number computations required anymore
- more efficient computation of usable rules
Version 2.32 (22 January 2018)
- support for persistent decomposition based (non-)confluence proofs
- faster checking of complexity proofs with matrix interpretations
- switch to Isabelle 2017
Version 2.31 (14 August 2017)
- proved that completion always succeeds if the input equations are ground and the employed reduction order is total on (equivalent) ground terms (moreover, every reduced ground TRS can be obtained by completion from any equivalent set of ground equations)
- terminating critical-pair-closing systems as confluence criterion
Version 2.30 (29 May 2017)
- support for non-linear integer transition systems in input
- hint-structure for lexicographic ranking functions
- support for multiple initial states in integer transition systems
- formalized correctness of abstract completion for infinite runs (fair infinite runs produce complete presentations of the initial equations) and similarly for ordered completion
Version 2.29 (23 February 2017)
- confluence of quasi-decreasing SDTRSs where all CCPs are joinable (contextual rewriting based criteria of context-joinability and unfeasibility)
- generatlized tcap (with symbol graph) for infeasibility
- removal of infeasible rules from CTRSs
- inlining of conditions of CTRSs
- support for integer transition systems: safety and termination proofs
- algebraic numbers with certified factorization algorithm (instead of oracle)
- switch to Isabelle 2016-1
Version 2.28 (11 October 2016)
- CeTA version from CoCo 2016
- improved error messages for rejected (non)confluence certificates
Version 2.27 (12 May 2016)
- conversion version of rule labeling as confluence criterion
Version 2.26 (15 April 2016)
- AC DP framework
- AC dependency pairs
- AC reduction pair processor with usable rules
- AC subterm criterion
- AC dependency graph
Version 2.25 (7 March 2016)
- parallel closed as confluence criterion
Version 2.24 (23 February 2016)
- level-confluence of conditional TRSs with infeasible critical pairs
- confluence of conditional TRSs via exact tree-automata completion (ancestor automaton)
- support for non-joinability and non-reachability proofs
- executable AC-equivalence checking
- precise computation of eigenvalues in complexity proofs for matrix interpretations via algebraic numbers
- new decision procedure for "is tree automaton closed under rewriting?" with witnesses in negative case
- non-termination proofs via tree automata
- switch to Isabelle 2016
Version 2.23 (13 October 2015)
- algebraic methods for matrix interpretations in complexity proofs without any restriction on shape
- basic support for matrix interpretations with constant complexity
Version 2.22 (30 August 2015)
- fixed bug in parsing non-termination assumptions
- bound for upper-triangular matrices in complexity proofs is now precise
Version 2.21 (27 June 2015)
- conditional confluence via almost-orthogonality modulo infeasible critical pairs
Version 2.20 (22 June 2015)
- basic term indexing integrated in dependency graph processor
- switch to Isabelle 2015
Version 2.19.1 (23 March 2015)
- conditional confluence via unravelings for ultra-left-linear CTRSs
- weak dependency pairs and dependency tuples as complexity technique
- usable rules and usable replacement maps as complexity technique
- relative termination and rule labeling as confluence technique
- addition and removal of redundant rules as (non-)confluence technique
- fixed efficiency problem of semantic labeling that was introduced with version 2.19
Version 2.18 (1 October 2014)
- equational proofs can now store lemmas
Version 2.17 (5 September 2014)
- improved usable rules for non-joinability
- matchbounds as complexity technique for standard and relative rewriting
- switch to Isabelle 2014
Version 2.16 (2 July 2014)
- restructured and extended tree automata theories
- decreasing diagrams in abstract setting
- rule labeling as confluence technique
Version 2.15 (26 May 2014)
- match-bounds technique does no longer require left-linearity
- uncurrying as non-termination technique
- grounding for non-confluence
- improved efficiency for size-change termination
- switched to Isabelle development version
Version 2.14.1 (30 April 2014)
- several new techniques for disproving confluence
- non-looping string-rewrite systems
- switch from innermost nontermination to nontermination for TRSs
- fixed problem in proof restructuring for unlabeling
- improved code equations for multiset operations
- make use of mutually recursive partial functions
- normalization equivalent reduced TRSs are unique up to renaming of variables
Version 2.13 (11 February 2014)
- support for forbidden patterns
- support for context-sensitive rewriting
- partial non-termination proofs
- improved checks for completeness of rewriting and narrowing
- soundness of abstract completion with prime critical pairs
Version 2.12 (23 January 2014)
- non-confluence via tree automata proofs
- allow different square-roots in interpretations
- support for unknown proof obligations
- switch to Isabelle 2013-2
Version 2.11 (21 October 2013)
- better support for partial proofs
- new tree automaton algorithms based on state-compatibility and state-coherence
- numbers of form a + b*sqrt(2) also for complexity
- switch to Isabelle 2013-1-RC-3
Version 2.10 (10 June 2013)
- interpretations using numbers of form a + b*sqrt(2) as carrier
- linear + strongly closed as confluence criterion
- bounded increase supports carriers over the rationals
- narrowing processor can be used in nontermination proofs
- rewriting processor can be used in nontermination proofs
- improved unification algorithm
Version 2.9 (14 February 2013)
- changed to Isabelle 2013
- subterm coefficient functions for KBO
- termination of KBO via Kruskal's tree theorem
- bounded increase with confluence instead of minimality
- complex constant removal (preprocessor of bounded increase)
Version 2.8.2 (7 January 2013)
- strongly linear interpretations for complexity
- termination by bounded increase
- termination of conditional rewriting via unravelings
- improved efficiency of CeTA, especially of parser
Version 2.7 (19 June 2012)
- weakened preconditions of narrowing processor
- more robust check for rewriting processor allowing variable renamings
- more robust check for semantic labeling in the innermost case
- combined size-change termination with innermost dependency graph
- improved error messages
Version 2.6 (15 June 2012)
- outermost nontermination proofs via rule removal and outermost loops
- support semantic labeling in the innermost case
- more robust checks for instantiation and forward instantiation processor
Version 2.5 (23 May 2012)
- weak orthogonality as confluence criterion
- support for non-confluence proofs using tcap or Newman's lemma
- support of innermost rewriting with normal form substitutions (for free variables on rhss)
- removal of trivial rules (s = s) for relative rewriting
- instantiation processor is complete
- improved non-loop checker
- changed to Isabelle 2012
Version 2.4 (19 April 2012)
- support for Knuth-Bendix orders
- support for complexity proofs: upper-triangular matrices, modular complexity via relative rewriting
- string-reversal for relative rewriting
- EIDG***
- switch from innermost to full rewriting for nontermination
- delete unused left-hand sides in strategy component
- non-looping nontermination
- monotone arctic matrix interpretations
- improved efficiency of size-change termination check
Version 2.3 (13 February 2012)
- improved efficiency of XML-parser
- improved error messages
Version 2.2 (15 January 2012)
- support of dms for SCNP reduction pairs
- improved error messages
Version 2.1 (20 December 2011)
- innermost usable rules in combination with reduction pairs
- certification of equational proofs and disproofs
Version 2.0 (17 November 2011)
- support for innermost rewriting
- dependency pair transformations narrowing, rewriting, instantiation, and forward-instantiation
- innermost dependency graph
- innermost usable rules
- switch to innermost termination (for locally confluent overlay systems)
- size-change in NP
- certification of confluence proofs
- certification of completion proofs
- partial termination proofs
- changed to Isabelle 2011-1
Version 1.20 (10 June 2011)
- support for recursive path order
Version 1.19 (24 May 2011)
- support for multiset path order
Version 1.18 (6 May 2011)
- supporting CPF version 2.1
- improved support of uncurrying
- match- and roof-bounds for left-linear TRSs
- improved root-labeling
Version 1.17 (20 February 2011)
- changed to Isabelle 2011
- use IsaFoR to prove termination of Isabelle functions, cf. TermFun
- code generation now also in Scala
Version 1.16 (13 January 2011)
- support for uncurrying
- support for quasi-models in semantic labeling
Version 1.15 (9 August 2010)
- improved check for (weak)-monotonicity of non-linear polynomial interpretations, allowing interpretations like 2x²-x+1
- fixed missing output of non-linear polynomial interpretations
- string reversal and flat context closure can now be used between labeling and unlabeling
Version 1.14 (8 July 2010)
- support for non-linear polynomial interpretations
Version 1.13 (24 June 2010)
- support for all relative termination techniques in CPF 2.0, except string reversal
- changed to Isabelle2009-2
Version 1.12 (31 May 2010)
- switch to CPF version 2.0
- nontermination proofs within the DP framework
Version 1.11 (14 April 2010)
- arctic semiring over (matrices over) the rationals
- flat context closure for DP problems with left-linear R-component (enabling a certified proof of Touzet's SRS)
Version 1.10 (17 March 2010)
- monotone matrix interpretations
- deletion of pairs and usable rules that have non-usable symbols in their left-hand side
Version 1.09 (22 January 2010)
- improved efficiency of size-change termination
- internal cleanup
Version 1.08 (14 December 2009)
- string reversal
- fixed variableConditionViolated parser bug (thanks Harald)
- changed to Isabelle2009-1
Version 1.07 (12 November 2009)
- changes in parser due to changes in CPF format
- lexicographic path order
- argument filters (which can also be used to permute arguments for LPO)
- rationals and matrices over rationals
- flat context closures for TRSs (but not yet for DPs)
Version 1.06 (30 September 2009)
- switch to CPF format
- polynomials over matrices
- arctic and arctic-below-0 domain
- root-labeling (but no flat context closures yet)
- size-change termination
- code generation now also in OCaml (in addition to Haskell)
Version 1.05 (28 July 2009)
- improved efficiency of dependency graph processor
- changes in format of unlabeling processor (now unlabeled DP problem has to be given)
Version 1.04 (22 June 2009)
- added subterm criterion
- added semantic labeling (finite carrier, models only)
Version 1.03 (7 May 2009)
- added reduction pair processor with usable rules regarding argument filter
- added monotonic reduction pair processor with usable rules
- added nontermination proof by just stating that the TRS is not well formed
- changed to Isabelle2009
Version 1.02 (21 April 2009)
- added monotonic reduction pairs
- added polynomial interpretations with negative constants
- changed to XML input/output
Version 1.01 (27 March 2009)
- improved error messages for loop proofs
Version 1.00, announced on termtools, (20 March 2009)
- added loop certification
- new implementation of (e)tcap based on maps (defsymbol -> rule set)
Version 0.99, initial version for TPHOLs paper, (13 March 2009)
- Dependency Pairs
- Dependency Pair Framework
- Dependency Graph Processor (EDG^***)
- Reduction Pair Processor with linear polynomial orders