## 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 *\$
```

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