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.