Packages

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

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

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.

Implements an algorithm for higher-order pre-unification.

Provides a Smart Cell for querying external provers on SystemOnTPTP.

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

MCP server exposing SystemOnTPTP theorem provers to Claude Code

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.