4 found
Sort by:
  1. Jeremy E. Dawson, A General Theorem on Termination of Rewriting.
    We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be handled by (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Jeremy E. Dawson, Embedding Display Calculi Into Logical Frameworks : Comparing Twelf and Isabelle.
    We compare several methods of implementing the display (sequent) calculus RA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise within the logical framework proof-theoretic results such as the cut-elimination theorem for RA and any associated increase in proof length. We discuss issues arising from this requirement.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  3. Jeremy E. Dawson, Formalised Cut Admissibility for Display Logic.
    We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  4. Jeremy E. Dawson, Machine-Checking the Timed Interval Calculus.
    We describe how we used the interactive theorem prover Isabelle to formalise and check the laws of the Timed Interval Calculus (TIC). We also describe some important corrections to, clarifications of, and flaws in these laws, found as a result of our work.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation