Production / April 22, 2018
(5.0/5) (2)
Loading...

Description

This application is a proof assistant for higher-order logic.Theprover kernel is based on HOL Light. The goal of this app istoenable the user a simple usage of an interactive theoremprover.The user interface is simple and self explaining to enableanefficient usage of the system. In the application there aretwoimportant parts which will be explained in the followinglines:Prover: is the main part of the application. Here you areable toobtain your theorems. First you have to build some terms inthe"Term Builder". With this terms and the the 10 inference rulesofHOL Light you are able to play around with the app. TermBuilder:is the part where you can build your terms. The constructedtermsare needed to start a proof. You have to be careful howtoconstruct terms. The only way to build terms is withlambdacalculus. For example if you want to build "x = x" then youhave toinput this: Comb(Comb(=,x),x). However after building terms,theywill be displayed in a more convenient style. All providedrulesfor constructing proofs are explained below: REFL: saysthatequality is reflexive. For this rule no preconditions areneeded.The only argument is a term TRANS: says that equalityistransitive. For this rule two theorems have to be provided.Theoutput of this rule is a theorem with transitivity applied.MK_COMBsays that equal functions applied to equal arguments giveequalresults. This rule takes two theorems as input. One says thattwofunctions (f,g) are equal, the other says that two arguments(x,y)are equal. A \theorem is returned where the functions f(x) andg(y)are equal. ABS: It is required that x is not a free variable inanyof the assumptions. If two expressions involving x are equal,thenthe functions that take x to those values are equal. BETA:Thisrule implements a simple version of beta reduction. ASSUME:saysthat from any p we can deduce p. This rule takes a term p oftypeboolean as an input. EQ_MP: connects equality withdeduction,saying that if \p and q are equal and it is possible todeduce p,then q can be deduced as well. This rule takes twotheorems as aninput and outputs a theorem with q as theconclusion.DEDUCT_ANTISYM_RULE: connects equality and deduction,saying thatif q can be deduced by p and vice versa, q and p areequal. INST:expresses that if p is true for variables x1,...,xnthen thosevariable can be replaced by any terms of the same types.INST_TYPE:works like INST but type variables will be substituted.

App Information HOL Theorem Prover

  • App Name
    HOL Theorem Prover
  • Package Name
    com.appsinprogress.hol_theorem_prover
  • Updated
    April 22, 2018
  • File Size
    1.4M
  • Requires Android
    Android 5.0 and up
  • Version
    Production
  • Developer
    AppsInProgress
  • Installs
    100+
  • Price
    Free
  • Category
    Education
  • Developer
  • Google Play Link

AppsInProgress Show More...

HOL Theorem Prover Production APK
This application is a proof assistant for higher-order logic.Theprover kernel is based on HOL Light. The goal of this app istoenable the user a simple usage of an interactive theoremprover.The user interface is simple and self explaining to enableanefficient usage of the system. In the application there aretwoimportant parts which will be explained in the followinglines:Prover: is the main part of the application. Here you areable toobtain your theorems. First you have to build some terms inthe"Term Builder". With this terms and the the 10 inference rulesofHOL Light you are able to play around with the app. TermBuilder:is the part where you can build your terms. The constructedtermsare needed to start a proof. You have to be careful howtoconstruct terms. The only way to build terms is withlambdacalculus. For example if you want to build "x = x" then youhave toinput this: Comb(Comb(=,x),x). However after building terms,theywill be displayed in a more convenient style. All providedrulesfor constructing proofs are explained below: REFL: saysthatequality is reflexive. For this rule no preconditions areneeded.The only argument is a term TRANS: says that equalityistransitive. For this rule two theorems have to be provided.Theoutput of this rule is a theorem with transitivity applied.MK_COMBsays that equal functions applied to equal arguments giveequalresults. This rule takes two theorems as input. One says thattwofunctions (f,g) are equal, the other says that two arguments(x,y)are equal. A \theorem is returned where the functions f(x) andg(y)are equal. ABS: It is required that x is not a free variable inanyof the assumptions. If two expressions involving x are equal,thenthe functions that take x to those values are equal. BETA:Thisrule implements a simple version of beta reduction. ASSUME:saysthat from any p we can deduce p. This rule takes a term p oftypeboolean as an input. EQ_MP: connects equality withdeduction,saying that if \p and q are equal and it is possible todeduce p,then q can be deduced as well. This rule takes twotheorems as aninput and outputs a theorem with q as theconclusion.DEDUCT_ANTISYM_RULE: connects equality and deduction,saying thatif q can be deduced by p and vice versa, q and p areequal. INST:expresses that if p is true for variables x1,...,xnthen thosevariable can be replaced by any terms of the same types.INST_TYPE:works like INST but type variables will be substituted.
Loading...