Zahra Ashktorab, Djallel Bouneffouf, et al.
IJCAI 2025
In order to establish that ℒ[A] = ℒ[B] follows from a set of assumptions Γ often one proves A =B and then invokes the principle of substitution of equals for equals. It has been observed that in the ancillary proof of A =B one is allowed to use, in addition to those assumptions of Γ which are free for ℒ, certain (open) sentences P which may not be part of Γ and may not follow from Γ, but are related to the context ℒ. We show that in an appropriate formal system there is a closed form solution to the problem of determining precisely what sentences P can be used. We say that those sentences hold in the context ℒ under the set of assumptions Γ. We suggest how the solution could be exploited in an interactive theorem prover. © 1993 Kluwer Academic Publishers.
Zahra Ashktorab, Djallel Bouneffouf, et al.
IJCAI 2025
Jungo Kasai, Kun Qian, et al.
ACL 2019
Arnold L. Rosenberg
Journal of the ACM
Imran Nasim, Melanie Weber
SCML 2024