F L i P proof checker reference

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

Logics

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.

Notation

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 Print 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.

Commands

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=[]): Check steps in proof script (not a file but an expression). Pretty-print each step as it is checked. If invalid step found, print error message and return False. If no invalid steps, after last step print nothing more and return True.
checkp(formula_arg, rule, *premises_etc): Check step and update proof state, pretty-print step, print error
rapply(rule, *premises_etc): Like checkp but no formula argument. Prover generates formula from rule, premises. For the Ae rule, must also provide a term or variable to substitute for the bound variable: 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): Back up: delete last n proof steps, just print warning if n bigger than proof
backa(): Back up past assumption: delete proof steps back through latest assumption
clear(): Start over, remove all proof steps
rules(): Print all rules: short name, premises, and conclusion. Does not show subproof structure of rules.
apropos(op): Print rules where op (operator) is main connective in premise or conclusion. Does not show subproof structure.
state(): Print entire proof state, list of steps as tuples
pp(): Print proof in Kaye's format ("pretty print")
ptree(index=len(steps)-1, indent=0): Print proof steps as tree with conclusion at top, premises indented below. Root of tree is step at index, start with given indent (n of spaces). Default prints whole proof.
save(name): Save current proof state in file. name is module name, not file name.

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)

Input	Print	Notes
Text('Any text')	Any text	Comment text, usually in step 0

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

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