bzhan / auto2

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

Please see doc.pdf for documentation.

Current version of the program works with Isabelle2021-1.

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.