Packages

Data structures for various HOL objects and TH0/1 parser.

Elixir client for automated theorem provers via SystemOnTPTP, StarExec, and Isabelle servers.

Higher-order pre-unification, Miller pattern unification, and second-order matching for ShotDs terms.

Livebook Smart Cells for AtpClient: a unified frontend over SystemOnTPTP, StarExec, Isabelle, and local TPTP-compliant prover binaries.

MCP server exposing the SystemOnTPTP, StarExec, Isabelle and LocalExec theorem-prover backends from AtpClient over stdio JSON-RPC.

An extention of the package HOL implementing the syntax of classical higher-order logic. Also includes a parser for TPTP TH0 syntax to the internal term representation of HOL.

Provides a Smart Cell for parsing TPTP Syntax into ShotDs data structures.

An Elixir implementation of NCPO-LNF (the βη-long-normal Computability Path Order of Niederhauser and Middeldorp) for ordering terms in Church's simple type theory as represented by the `shot_ds` library.

Tableau component of Shot, a parallel Church Simple Type Theory theorem prover.