The CiME3 system
Version 3.0beta

Evelyne Contejean, Pierre Courtieu , Julien Forest, Olivier Pons and Xavier Urbain
CNRS-LRI-Universite Paris Sud XI
Cedric-CNAM-ENSIIE
INRIA Saclay-Île-de-France

Chapter 1  Tutorial

This chapter is a small tutorial, to present the basic features of CiME in a progressive way.

• The toplevel language
  • Expressions
  • Definitions with let
  • Definitions of functions
  • Higher-order functions
• More toplevel user interaction
  • Loading expressions from files
  • Interrupting evaluation
  • Time spent in computation
  • Quitting CiME
• Definition of first-order signatures
• Definition of Algebra
• Definition of terms
  • Terms manipulation
• Rewriting
• Checking termination of rewrite systems
  • Producing proof trace and proof certificate
  • Giving a strategy
    • Specifying Ordering Parameters
    • Combining criteria
• Checking confluence of rewrite systems
• Proofs of equality
• String rewriting
• Using CiME in Batch Mode
  • Input formats
  • Output format

Index

This document was translated from L^AT_EX by H^EV^EA.