F L i P Home Download User's guide Logics Code Tests Notes PyPI GitHub
Flip is a logical framework written in Python. One Flip application is a natural deduction proof checker. This is its reference manual; there is also a user's guide.
Logics Notation Commands Error messages Bibliography
The checker can use different logics; Flip comes with several, and you can define more. To use a logic, run its session module in the Python session, for example:
python -i -m flip.logic.fol_session >>>
These session modules are included with Flip:
tree_session | Tree logic from Kaye chapter 3 |
poset_session | Poset logic from Kaye chapter 4 |
prop_session | Propositional logic from Kaye chapter 6 |
prop_constructive_session | Constructive propositional logic from Bornat chapter 3 |
prop_derived_session | Propositional logic with derived rules from Huth and Ryan chapter 1 |
fol_session | First-order logic from Kaye chapter 9 (includes propositional rules) |
fol_derived_session | First-order logic from Huth and Ryan chapter 2 (includes prop_derived rules) |
The rules command prints all the inference rules available in a session. The rule_names attribute is a dictionary that associates each rule with its description.
Starting with version 1.2, it is also possible to use the poset logic with this command:
python -i -m flip.poset.session >>>
This will be the recommended way to use logics added after version 1.2.
Flip only uses characters found on a standard (Roman) keyboard; it does not use mathematical symbols. For example, for and and or Flip prints & and v rather than symbols that look like /\ and \/.
At this writing Flip does not provide a parser. Flip reads formulas in a prefix constructor syntax that differs from its printed syntax. For example, we write And(p,q) instead of p & q.
The following tables show how to notate formulas in the Flip logics.
All logics:
Input | Notes | |
Text('Any text') | Any text | Comment text, usually in step 0 |
Tree logic:
Path('01') | 01 | any sequence of 0 or 1 |
Poset logic:
F | F | Bottom |
lt(a,b) | a < b | |
nlt(b,a) | b /< a |
Poset elements a, b, c, d are defined. To define another: e = Variable('e')
Propositional logics:
F | F | Bottom, false |
T | T | Top, true |
Not(p) | ~p | not p |
And(p,q) | p & q | p and q |
Or(p,q) | p v q | p or q |
Impl(p,q) | p -> q | p implies q |
Propositional letters (Boolean variables) a, b, c, d, e, f, p, q, r, t are defined. To define another: s = Letter('s')
First order logics (also include propositional logic formulas):
Equal(x,y) | x = y | x equals y |
A(x,P(x)) | Ax.P(x) | universal quantifier: for all x, P(x) |
E(x,P(x)) | Ex.P(x) | existential quantifier: there exists x, such that P(x) |
New(x) | Let x be arbitrary | new variable for subproof |
Let(x,P(x)) | Let x satisfy P(x) | assumption, with new variable |
Propositional letters e, p, q, r and variables a, b, c, d, t, u, v, w, x, y, z are defined. To define another, f = Letter('f') or s = Variable('s'). Variables and Letters can be any length; they need not be limited to one character.
Functions f, g, h and relations P, Q, R, S are defined. They can take any number of arguments. To add another, we must define a new class that inherits Function or Relation.
The dir command prints identifiers available in a session, including all the operators, letters, variables, functions and relations.
These are the functions intended to be used as prover commands.
Some built-in Python functions are helpful as well:
dir
, help
, pprint
,
import
.
check_proof(script=[])
checkp(formula_arg, rule, *premises_etc)
rapply(rule, *premises_etc)
rapply(Ae, 1, x)
.
For the Ei rule, must also provide a dictionary that shows how to replace the term (key) with the bound variable (value):
rapply(Ei, 1, {x:v})
back(n=1)
backa()
clear()
rules()
apropos(op)
state()
pp()
ptree(index=len(steps)-1, indent=0)
save(name)
The dir command prints identifiers available in a session, including all the command names.
These are the error messages printed by the checker. Syntax error messages are printed by the the Python interpreter.
Errors in formula constructor arguments:
argument %s is not a string %s requires %d arguments, found %d %s argument %d, %s is %s, must be %s path %s does not match [01]*$
Errors in command arguments:
%s is %s, must be Formula cannot apply %s rule, must provide formula apply command requires argument: term or variable apply command requires argument: {term:variable}
Errors in premises:
requires %d premises, found %d no line %d for premise at index %d premise at index %d, line %d not in scope premise at index %d, line %d not an assumption premise at index %d, line %d not in same scope as assumption assumption at index %d, line %d not in scope for discharging rule
Errors in free or bound variables:
%s term %s includes bound variable in %s variable %s already appears free in proof among %s
Errors matching premises and formula to inference rule:
%s does not match %s with %s not all occurrences substituted the same way %s
The Flip logics are based on logics in these books:
Kaye, The Mathematics of Logic
http://web.mat.bham.ac.uk/R.W.Kaye/logic/
Huth and Ryan, Logic in Computer Science
http://www.cs.bham.ac.uk/research/projects/lics/
Bornat, Proof and Disproof in Formal Logic
http://www.oup.com/uk/catalogue/?ci=9780198530275