An Isabelle/HOL Formalization of Rewriting 
for Certified Tool Assertions 
Overview Developers Input Format Related Work Versions Experiments TermFun
Contents
News Introduction Publications Downloads Contact IsaFoR/CeTA Macros Old News

News

Introduction

Welcome to the IsaFoR/CeTA website.

CeTA is a tool that certifies (non)termination or (non)confluence or (non)commutation or completion or complexity proofs provided by some automated (termination/complexity/...) tool.

The development is supported by the following projects of the Austrian Science Fund (FWF):

It mainly consists of two parts.

  1. An Isabelle/HOL formalization of abstract results and concrete techniques from the rewriting literature, in form of the IsaFoR (Isabelle Formalization of Rewriting) library. Currently the following techniques are supported:
    • Termination (rewrite systems, relative rewrite systems, conditional rewrite systems, rewriting modulo AC, integer transition systems):
      • Dependency Pairs (incl. Dershowitz' refinement)
      • Dependency Pair Framework
      • Dependency Graph Processor (E(I)DG***-estimation, i.e., using tcap and using both forward and backward directions, and in the innermost case additionally icap)
      • Reduction Pair Processors in several variants
      • Polynomial interpretations over naturals, rationals, arctic and arctic-below-zero semiring, and over matrices of all these domains. Moreover, for interpretations over the rationals and naturals, negative constants are allowed.
      • Max-polynomial interpretations over natural numbers.
      • Lexicographic, multiset, and recursive path order with argument filters and arbitrary permutations of arguments
      • Knuth-Bendix order with subterm coefficient functions, argument filters and arbitrary permutations of arguments
      • Weighted Path Order
      • Usable Rules (also with respect to argument filterings)
      • Subterm Criterion
      • Semantic Labeling
      • Flat Context Closure (for every TRS and for DP problems with left-linear R-component)
      • Root-Labeling
      • Size-Change Termination (also the Size-Change in NP variant which allows to delete only some pairs)
      • String Reversal
      • Uncurrying
      • Match- and roof-bounds
      • Switch between full and innermost rewriting
      • DP Transformations Narrowing, Rewriting, and (Forward)-Instantiation
      • Bounded Increase
      • Unravelings
      • Cooperation Graphs
      • Lexicographic ranking functions
      • Invariants via Impact algorithm
      • Fresh variable and location addition
      • SCC decomposition of program graph
    • Nontermination (rewrite systems and relative rewrite systems):
      • Loops (also for innermost and outermost strategy and forbidden patterns)
      • Non-looping infinite rewrite sequences
      • Regular languages which are closed under rewriting and do not contain normal forms
      • TRSs violating the variable condition
      • String reversal
      • Rule removal
      • Dependency pairs
      • DP Transformations Narrowing, Rewriting, and (Forward)-Instantiation
      • Switch from innermost to full rewriting
      • Partial nontermination proofs
    • Complexity:
      • Weak dependency pairs and dependency tuples
      • Usable rules and usable replacement maps
      • Strongly linear polynomial interpretation (in case of runtime complexity: arbitrary interpretations for defined symbols)
      • Matrix interpretations of arbitrary shape
      • Runtime complexity and derivational complexity
      • Rule shifting for relative rewriting
      • (Relative) Matchbounds
    • Confluence and non-confluence (several techniques are also available for commutation and non-commutation):
      • Unravelings for ultra left-linear deterministic conditional TRSs of type 3
      • Addition and removal of redundant rules
      • Rule labeling and relative termination (valley and conversion versions)
      • Local confluence via critical pairs
      • Weak orthogonality
      • Development closed
      • Parallel critical pairs closed
      • Linear + strongly closed
      • Left-linear + almost parallel closed
      • Terminating critical-pair-closing systems
      • Non-joinable forks using tcap, tree automata techniques, usable rules, interpretations, or discrimination pairs
      • Modularity of non-confluence
      • Newman's Lemma
      • Persistent decomposition
      • Compositional criteria based on parallel critical pairs
    • Completion:
      • Requires rewrite sequences how to obtain R from E, and a termination proof of R
      • Ordered completion
    • Equational Reasoning:
      • Birkhoff's theorem
      • certification via completed rewrite system, proof tree using equational logic, or derivation
    • Safety:
      • Invariants via Impact algorithm
  2. The certifier CeTA, an automatically generated Haskell program (using the code generation feature of Isabelle) for certifying proofs.

Publications

Downloads

The current version is 3.0.1. To access previous versions of CeTA and see the differences please visit this site.

Binaries of our tool are available for the following platforms:

Alternatively, you may download the source-code for CeTA. Please have a look into the README for installation instructions.

You can directly browse or download the sources of all releases and the current development snapshot of our Isabelle-formalization IsaFoR in the Mercurial repository.

Contact

For general questions to the developers send a mail to ceta@informatik.uibk.ac.at. You can also subscribe and send messages to the CeTA users mailing list where your messages will be posted to all CeTA users, and where the developers will inform you about updates, ... .

LaTeX Macros for Typesetting IsaFoR/CeTA

In order to refer to our library and our certifier in your LaTeX documents correctly, please use the following macros: 
\newcommand\isafor{\textsf{Isa\kern-0.15exF\kern-0.15exo\kern-0.15exR}}
\newcommand\ceta{\textsf{C\kern-0.15exe\kern-0.45exT\kern-0.45exA}}
The results should look approximately as follows:

Old News