HOL Theorem Prover APK

Bugfix

This application is a proof assistant for higher-order logic. The prover kernel is based on HOL Light. The goal of this app is to enable the user a simple usage of an interactive theorem prover. The user interface is simple and self explaining to enable an efficient usage of the system.


In the application there are two important parts which will be explained in the following lines:

Prover: is the main part of the application. Here you are able to obtain your theorems. First you have to build some terms in the "Term Builder". With this terms and the the 10 inference rules of HOL Light you are able to play around with the app.

Term Builder: is the part where you can build your terms. The constructed terms are needed to start a proof. You have to be careful how to construct terms. The only way to build terms is with lambda calculus. For example if you want to build "x = x" then you have to input this: Comb(Comb(=,x),x). However after building terms, they will be displayed in a more convenient style.


All provided rules for constructing proofs are explained below:

REFL: says that equality is reflexive. For this rule no preconditions are needed. The only argument is a term

TRANS: says that equality is transitive. For this rule two theorems have to be provided. The output of this rule is a theorem with transitivity applied.

MK_COMB says that equal functions applied to equal arguments give equal results. This rule takes two theorems as input. One says that two functions (f,g) are equal, the other says that two arguments (x,y) are equal. A \theorem is returned where the functions f(x) and g(y) are equal.

ABS: It is required that x is not a free variable in any of the assumptions. If two expressions involving x are equal, then the functions that take x to those values are equal.

BETA: This rule implements a simple version of beta reduction.

ASSUME: says that from any p we can deduce p. This rule takes a term p of type boolean as an input.

EQ_MP: connects equality with deduction, saying that if \p and q are equal and it is possible to deduce p, then q can be deduced as well. This rule takes two theorems as an input and outputs a theorem with q as the conclusion.

DEDUCT_ANTISYM_RULE: connects equality and deduction, saying that if q can be deduced by p and vice versa, q and p are equal.

INST: expresses that if p is true for variables x1,...,xn then those variable can be replaced by any terms of the same types.

INST_TYPE: works like INST but type variables will be substituted.