Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Missing weak supplementation axiom for occurrents #126

Open
alanruttenberg opened this issue Jan 27, 2025 · 2 comments
Open

Missing weak supplementation axiom for occurrents #126

alanruttenberg opened this issue Jan 27, 2025 · 2 comments
Assignees
Labels
bug Something isn't working

Comments

@alanruttenberg
Copy link
Contributor

It was failing in the model so I removed it with the intention of fixing the model at some point, but never got back to it.
There is weak supplementation only for temporal regions.

@alanruttenberg alanruttenberg added the bug Something isn't working label Jan 27, 2025
@michaelrabenberg
Copy link

Each of the extant weak-supplementation axioms, vbw-1 and fyf-1, has a (instance-of _ temporal-region _) clause in the antecedent that I think is unnecessary. For example take fyf-1; I've boldfaced the clause I have in mind:

(cl:comment "continuant-part-of has weak supplementation [fyf-1]"
(forall (t x y)
(if
(and (instance-of x continuant t) (instance-of y continuant t)
(instance-of t temporal-region t))
(if (and (continuant-part-of x y t) (not (= x y)))
(exists (z)
(and (instance-of z continuant t) (continuant-part-of z y t)
(not (= z y))
(not
(exists (overlap)
(and (instance-of overlap continuant t)
(continuant-part-of overlap x t)
(continuant-part-of overlap z t))))))))))

What of importance would be lost if the boldfaced clause and the analogous one in vbw-1 were deleted and any consequently necessary adjustments were made? (With this one I think you can just delete the clause and that's that (haven't checked) but with the other one I think a quantified variable needs to be deleted.)

@michaelrabenberg
Copy link

Another seemingly deletable clause in boldface; another clause in italics for reasons stated below:

(cl:comment "continuant-part-of has weak supplementation [fyf-1]"
(forall (t x y)
(if
(and (instance-of x continuant t) (instance-of y continuant t)
(instance-of t temporal-region t))
(if (and (continuant-part-of x y t) (not (= x y)))
(exists (z)
(and (instance-of z continuant t) (continuant-part-of z y t)
(not (= z y))
(not
(exists (overlap)
(and (instance-of overlap continuant t)
(continuant-part-of overlap x t)
(continuant-part-of overlap z t))))))))))

The boldfaced clause is entailed by the italicized one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants