Packages
shot_ds
1.3.1Data structures for various HOL objects and TH0/1 parser.
atp_client
0.6.2Elixir client for automated theorem provers via SystemOnTPTP, StarExec, and Isabelle servers.
shot_un
0.2.1Higher-order pre-unification, Miller pattern unification, and second-order matching for ShotDs terms.
kino_atp_client
0.6.0Livebook Smart Cells for AtpClient: a unified frontend over SystemOnTPTP, StarExec, Isabelle, and local TPTP-compliant prover binaries.
atp_mcp
0.5.1MCP server exposing the SystemOnTPTP, StarExec, Isabelle and LocalExec theorem-prover backends from AtpClient over stdio JSON-RPC.
behold
1.1.3An 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.
kino_shot_ds
0.1.3Provides a Smart Cell for parsing TPTP Syntax into ShotDs data structures.
shot_to
0.2.0An 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.
shot_tx
0.1.0Tableau component of Shot, a parallel higher-order theorem prover.
tptp
0.1.0A faithful, span-carrying parser, linter and printer for the TPTP language.