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

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.

The dir command prints identifiers available in a session, including all the command names.

Error messages

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
```

Bibliography

The Flip logics are based on logics in these books:

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

F L i P Home   Download   User's guide   Reference   Logics   Code   Tests   Notes   PyPI   GitHub