cl-banner

CeTA


News

  • 29th April 2020: IsaFoR/CeTA version 2.39 has been released.
  • 19th December 2019: IsaFoR/CeTA version 2.38 has been released.
  • 20th June 2019: IsaFoR/CeTA version 2.37 has been released.
  • 1st April 2019: IsaFoR/CeTA version 2.36 has been released.
  • 26th December 2018: IsaFoR/CeTA version 2.35 has been released.


Introduction

Welcome to the IsaFoR/CeTA website.

CeTA is a tool that certifies (non)termination or (non)confluence 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:


  • 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
  • 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

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
  • Certified ACKBO
    A. Lochmann and C. Sternagel
    Proc. of the 8th International Conference on Certified Programs and Proofs (CPP '19), ACM, pages 144–151, 2019.
  • Infinite Runs in Abstract Completion
    N. Hirokawa, A. Middeldorp, S. Winkler, and C. Sternagel
    Proc. of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD '17), LIPIcs 84, pages 19:1–19:16, 2017.
  • Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
    C. Sternagel and T. Sternagel
    Proc. of the 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pages 413–431, 2017.
    © Springer-Verlag
  • AC Dependency Pairs Revisited
    A. Yamada, C. Sternagel, R. Thiemann, and K. Kusakari
    In Proc. of the 25th EACSL Annual Conference on Computer Science Logic (CSL'16), LIPIcs 62, pages 8:1–8:16, 2016.
  • Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
    J. Nagele and A. Middeldorp
    In Proc. of the 7th International Conference on Interactive Theorem Proving (ITP'16), LNCS 9807, pages 290–306, 2016.
    © Springer-Verlag
  • Algebraic Numbers in Isabelle/HOL
    R. Thiemann and A. Yamada
    In Proc. of the 7th International Conference on Interactive Theorem Proving (ITP '16), Lecture Notes in Computer Science 9807, pages 391-408, 2016. © Springer-Verlag
  • Formalizing Jordan Normal Forms in Isabelle/HOL
    R. Thiemann and A. Yamada
    In Proc. of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '16), pages 88-99, 2016.
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016
  • Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems
    F. Rapp and A. Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    LIPIcs 52, pp. 36:1 – 36:12, 2016


Contact

For questions or feedback please contact Franziska Rapp or Aart Middeldorp.
 

Nach oben scrollen