README

Copyright (C) 2013 Korei Klein <korei.klein1@gmail.com>

SUMMARY:
  Fantasia is an interactive proof tool containing an embedded program extraction engine.
  Fantasia first assists its user in constructing a proof, and then converts the proof into
  a program for calculating whatever the proof shows.


THE QR DEMO:
  This version of Fantasia contains a demo proof of the quotient-remainder theorem.

  The quotient remainder theorem states that
    for every pair of natural numbers (A,B), if b != 0, then there exists
    a quotient Q and a remainder R such that R < b and A = R + Q * B.

  The quotient remainder theorem can be proved by mathematical induction on B, and the
  resulting proof can be converted via extraction into a program that calculates
  division and modulus operations.

RUNNING THE QR DEMO:
  To run the demo, type
    make

  You can modify the proof from the demo yourself by editing
  examples/QR.py and then running
    make

  You can check and modify the way the proof is printed out by examining ui/run/text/static.py.

RUNNING THE TESTS:
  To run the tests, type
    make test

  See tests/complete_suite.py to track down which tests are being run.