OSHL-S is an automated theorem prover
based on the OSHL algorithm. The current version of
OSHL-S includes a few extensions to the original algorithm, such as
types,
relaxed ordering, caching, etc..
One of the roles that a type system play in a programming language
is to eliminate expressions that lead to an error or diverge before
they are evaluated. The same idea can be applied to a set of first
order
clauses: constructing a type system that eliminates instances that are
not needed to find a refutation proof before starting searching for the
proof. A type system that generates terms using context free grammar,
CFT, is implemented in OSHL-S v0.5.0. The type inference engine
analyzes the input clause and infers the type of each free variable.
Types are used to restrict instantiation of clauses to a subset of
their instances, thereby reducing the search space. CFT is strictly
stronger than Simple Sort Inference. A paper describing the general
framework and details of CFT is submitted to CADE22 for review.
source
user manual
source
user manual