Fantasia is an interactive proof tool with an embedded program extraction engine. This repository is a read-only mirror; it does not answer pull requests. Contact Korei Klein <korei.klein - [at] - gmail.com> to inquire about becoming a contributor.
License: Other
Python 100.00%
fantasia's Introduction
Copyright (C) 2013 Korei Klein <[email protected]>
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.