Home / Education Apps / HOL Theorem Prover on Windows Pc

HOL Theorem Prover on Windows Pc

Developed By: AppsInProgress

License: Free

Rating: 5,0/5 - 1 votes

Last Updated: December 26, 2023

Compatible with Windows 10/11 PC & Laptop

App Details

Version	Production
Size	1.4 MB
Release Date	April 23, 18
Category	Education Apps
What's New: Bugfix [see more]
Description from Developer: 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 t... [read more]

App preview ([see all 5 screenshots])

About this app

On this page you can download HOL Theorem Prover and install on Windows PC. HOL Theorem Prover is free Education app, developed by AppsInProgress. Latest version of HOL Theorem Prover is Production, was released on 2018-04-23 (updated on 2023-12-26). Estimated number of the downloads is more than 10. Overall rating of HOL Theorem Prover is 5,0. Generally most of the top apps on Android Store have rating of 4+. This app had been rated by 1 users, 1 users had rated it 5*, 1 users had rated it 1*.

How to install HOL Theorem Prover on Windows?

Instruction on how to install HOL Theorem Prover on Windows 10 Windows 11 PC & Laptop

In this post, I am going to show you how to install HOL Theorem Prover on Windows PC by using Android App Player such as BlueStacks, LDPlayer, Nox, KOPlayer, ...

Before you start, you will need to download the APK/XAPK installer file, you can find download button on top of this page. Save it to easy-to-find location.

[Note] You can also download older versions of this app on bottom of this page.

Below you will find a detailed step-by-step guide, but I want to give you a fast overview of how it works. All you need is an emulator that will emulate an Android device on your Windows PC and then you can install applications and use it - you see you're playing it on Android, but this runs not on a smartphone or tablet, it runs on a PC.

If this doesn't work on your PC, or you cannot install, comment here and we will help you!

Install using BlueStacks
Install using NoxPlayer

Step By Step Guide To Install HOL Theorem Prover using BlueStacks

Download and Install BlueStacks at: https://www.bluestacks.com. The installation procedure is quite simple. After successful installation, open the Bluestacks emulator. It may take some time to load the Bluestacks app initially. Once it is opened, you should be able to see the Home screen of Bluestacks.
Open the APK/XAPK file: Double-click the APK/XAPK file to launch BlueStacks and install the application. If your APK/XAPK file doesn't automatically open BlueStacks, right-click on it and select Open with... Browse to the BlueStacks. You can also drag-and-drop the APK/XAPK file onto the BlueStacks home screen
Once installed, click "HOL Theorem Prover" icon on the home screen to start using, it'll work like a charm :D

[Note 1] For better performance and compatibility, choose BlueStacks 5 Nougat 64-bit read more

[Note 2] about Bluetooth: At the moment, support for Bluetooth is not available on BlueStacks. Hence, apps that require control of Bluetooth may not work on BlueStacks.

How to install HOL Theorem Prover on Windows PC using NoxPlayer

Download & Install NoxPlayer at: https://www.bignox.com. The installation is easy to carry out.
Drag the APK/XAPK file to the NoxPlayer interface and drop it to install
The installation process will take place quickly. After successful installation, you can find "HOL Theorem Prover" on the home screen of NoxPlayer, just click to open it.

Discussion

(*) is required

Download older versions

Other versions available: Production.

Download HOL Theorem Prover Production on Windows PC – 1.4 MB

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.

Bugfix