Logic

First-order logic reasoning with theorem proving, model finding, and syntax validation using Tau-Prolog.

First-order logic reasoning server built with Tau-Prolog that provides theorem proving, model finding, and syntax validation capabilities for logical formulas. Supports Prover9-style syntax with quantifiers, connectives, predicates, and functions, offering tools to prove statements using resolution, find finite models satisfying premises, discover counterexamples, and validate formula syntax with helpful error messages. Includes specialized support for category theory with axiom generation for categories, functors, monoids, and groups, plus diagram commutativity verification.