A best-first-search theorem prover implemented in Isabelle
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
FOL
HOL
document
.gitignore
README
ROOT
auto2.ML
auto2_data.ML
auto2_outer.ML
auto2_state.ML
box_id.ML
consts.ML
doc.pdf
items.ML
logic_steps.ML
matcher.ML
normalize.ML
proofsteps.ML
property.ML
propertydata.ML
rewrite.ML Header of ML files. Sep 11, 2018
status.ML
util.ML
util_base.ML
util_logic.ML Header of ML files. Sep 11, 2018
wellform.ML
wfdata.ML
wfterm.ML

README

AUTO2 - a best-first-search theorem prover implemented in Isabelle

Please see doc.pdf for documentation.

Current version of the program works with Isabelle2017.

Papers:

Efficient verification of imperative programs using auto2 (TACAS
2018): https://arxiv.org/abs/1610.06996. Code at v0.3 (0774b32).

Formalization of the fundamental group in untyped set theory using
auto2 (ITP 2017): https://arxiv.org/abs/1707.04757. Code at v0.2
(60daebd).

AUTO2, a saturation-based heuristic prover for higher-order logic (ITP
2016): http://arxiv.org/abs/1605.07577. Code at v0.1 (18b96cb).

Description of the examples:

- HOL/Functional: verification of functional programs. Include material
  on lists, trees, priority queue, Dijkstra's algorithm, and rectangle
  intersection.

- HOL/Imperative: verification of imperative programs using separation
  logic. Foundation of separation logic, and several of the examples,
  follow "A Separation Logic Framework for Imperative HOL" in Isabelle
  AFP.

- HOL/Primes_Ex: elementary number theory of primes, up to the proof
  of infinitude of primes and the unique factorization
  theorem. Follows theories Primes and UniqueFactorization in
  HOL/Number_Theory.

- HOL/Hoare: development of Hoare logic. Follows chapters Imp, Equiv,
  Hoare, and Hoare2 in "Software Foundations".

- FOL: axiomatic set theory based on Isabelle/FOL. Sources:

  - Basic set theory and construction of natural numbers: Isabelle/ZF.

  - More set theory: "Theory of Sets" by Bourbaki chapter II and part
    of chapter III.

  - Basic group theory and construction of real numbers: corresponding
    examples in HOL.

  - Arrow impossibility theorem: following Arrow_Order in
    AFP/ArrowImpossibilityGS. The original theory is one of seven test
    cases in "Sledgehammer: Judgement Day".

  - Point-set topology and construction of the fundamental group:
    "Topology" by Munkres.

Copyright (C) 2015-2017 Bohua Zhan

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or (at
your option) any later version.