Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Deriving logic programs from equational theories

Email Gateway (Jul 14 2025 at 17:15):

From: Patrick Nicodemus <gadget142@gmail.com>
Suppose I have an equational theory which includes, in addition to the
usual axioms $\forall x_1, ..., x_n, t_1= t_2$ I also have some axioms of
the form $\forall x_1, ..., x_n, t_1= t_2 \iff s_1 = s_2$. ($t_1$ has
the same variables as $s_1$.) Is there an algorithm I can use to orient
the iffs into ifs or only ifs, in such a way that I get a rewrite system
which is complete for the equational logic? (Not in general of course but
in good cases.)

By reducing the iffs to ifs, I get a Horn clause, so my perspective is that
I'm trying to derive a logic program from a presentation of an equational
theory, such that the logic program is sound and complete for the theory.

Reminds me of Knuth Bendix completion but it seems like a different problem.

More generally given a theory whose axioms are predicate equivalences
$\forall x_1, ..., x_n,p(t_1...t_k) \iff q(s_1 ... s_k)$ and $$forall
x_1,... x_n, p(t_1,...t_n)$$ I want to orient the iffs in a way that I can
rewrite my predicate and when it eventually ends up in normal form it is
either unifiable with an axiom (and is true) or not (and is false). Again,
a kind of logic program where every Horn clause has either zero or one
assumptions. Can somebody tell me more about this problem and where it is
referenced in literature?

Email Gateway (Jul 15 2025 at 07:40):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear Patrick,

Your problem seems to be related to a special case of the superposition calculus. Superposition is itself a kind of successor of Knuth-Bendix completion. To use superposition, you would need to replace each "iff" by two clauses. You also need to choose a term order, which can be used to tweak the ordering of the equations.

Superposition is (refutationally) complete. Various fragments are even decidable. Maybe if, given a problem, you can find a suitable term order, then you might get good behavior.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 14. Jul 2025, at 19:14, Patrick Nicodemus <gadget142@gmail.com> wrote:

Suppose I have an equational theory which includes, in addition to the usual axioms $\forall x_1, ..., x_n, t_1= t_2$ I also have some axioms of the form $\forall x_1, ..., x_n, t_1= t_2 \iff s_1 = s_2$. ($t_1$ has the same variables as $s_1$.) Is there an algorithm I can use to orient the iffs into ifs or only ifs, in such a way that I get a rewrite system which is complete for the equational logic? (Not in general of course but in good cases.)

By reducing the iffs to ifs, I get a Horn clause, so my perspective is that I'm trying to derive a logic program from a presentation of an equational theory, such that the logic program is sound and complete for the theory.

Reminds me of Knuth Bendix completion but it seems like a different problem.

More generally given a theory whose axioms are predicate equivalences $\forall x_1, ..., x_n,p(t_1...t_k) \iff q(s_1 ... s_k)$ and $forall x_1,... x_n, p(t_1,...t_n)$ I want to orient the iffs in a way that I can rewrite my predicate and when it eventually ends up in normal form it is either unifiable with an axiom (and is true) or not (and is false). Again, a kind of logic program where every Horn clause has either zero or one assumptions. Can somebody tell me more about this problem and where it is referenced in literature?

Last updated: Jul 26 2025 at 12:43 UTC