Email Gateway (Sep 07 2025 at 19:18): Email Gateway (Sep 07 2025 at 19:18):From: Patrick Nicodemus <gadget142@gmail.com>
The equational fragment of first-order logic is well studied in automated
theorem proving. I'm interested in what work has been done on "generalized
algebraic theories" which is a kind of first-order equational fragment of
dependent type theory. This is known to be equivalent to a fragment of
multi-sorted first order logic where you have a finite number of sorts A,
B, C, and functions p : B-> A, q : C -> A expressing how families of sets
B_a and C_a vary with a. A function f :\prod_a : B_a x B_a -> C_a is then
modeled as a (partial) functional relation R \subset B x B x C such that
R(b,b',c) -> p(b)=p(b')=q(c). So it's basically multi-sorted equational
logic with partial functions whose domains are also constrained by
equations. Can anyone send me resources on deciding equalities in this
theory? Are there any existing plugins or tools that carry out these
translations into FOL automatically?
Email Gateway (Sep 09 2025 at 13:47):From: Till Mossakowski <till.mossakowski@ovgu.de>
Such a logic has been developed by Horst Reichel in his book "Initial
computability, algebraic specifications, and partial algebras". A
translation to FOL has been implemented in Hets, see http://hets.eu
Am 07.09.25 um 21:17 schrieb Patrick Nicodemus:
The equational fragment of first-order logic is well studied in
automated theorem proving. I'm interested in what work has been done
on "generalized algebraic theories" which is a kind of first-order
equational fragment of dependent type theory. This is known to be
equivalent to a fragment of multi-sorted first order logic where you
have a finite number of sorts A, B, C, and functions p : B-> A, q : C
-> A expressing how families of sets B_a and C_a vary with a. A
function f :\prod_a : B_a x B_a -> C_a is then modeled as a (partial)
functional relation R \subset B x B x C such that R(b,b',c) ->
p(b)=p(b')=q(c). So it's basically multi-sorted equational logic with
partial functions whose domains are also constrained by equations. Can
anyone send me resources on deciding equalities in this theory? Are
there any existing plugins or tools that carry out these translations
into FOL automatically?
Last updated: Sep 13 2025 at 04:22 UTC