Skip to content

Conversation

wdcraft01
Copy link
Collaborator

@wdcraft01 wdcraft01 commented Aug 23, 2025

This branch provides a minor update to the Exists().eliminate() method, with the following 2 main changes:

  • reinstate a small block of code (performing a generalization step) that had been previously commented-out. Although automation can handle the generalization step, some experimentation suggested that an explicit call without relying on automation can save some substantial search/computation effort;
  • add a check and error message for cases when the eliminate() method is called prematurely when one or more of the Skolem constants still appear as a free variable in the targeted judgment.

The changes were tested with some simple examples in the existential demonstrations notebook but then the examples were deleted to keep this branch as clean as possible.

Update the Exists().eliminate() method to once again include an explicit generalization step that had been previously commented-out. Although the generalization can be handled through automation, some experimentation has shown that an explicit generalization call can substantially reduce the search and computational effort produced when relying solely on the automation.
Update the Exists().eliminate() method to explicitly catch cases where one or more of the Skolem constants still appear as free variable(s) in the targeted judgment, and to return an informative error message when this happens.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant