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

Update skolemize.py #2999

Open
wants to merge 22 commits into
base: develop
Choose a base branch
from
Open

Update skolemize.py #2999

wants to merge 22 commits into from

Conversation

cestwc
Copy link
Contributor

@cestwc cestwc commented May 7, 2022

add a function, richardize (just a name trying to make it not confused with simplify or __reduce__ ), modified from skolemize.

The function name does not represent any logician Richard, and maybe the NLTK maintenance party can choose a better name.
The new function changes minimum from skolemize, and instead conversion to CNF (which is not equivalent but equisatisfiable to the input FOL expression), richardize(your_expr).equiv(your_expr) will be True.

The motivation of this function is that I did not find simplify to work in the way I wished, and for a pretty messy expression, e.g., those with a lot of consecutive negations, the new function can make it neater.

@stevenbird
Copy link
Member

@cestwc: it looks like you've duplicated skolemize and made some changes to it. We need a well argued case for having (and maintaining) two similar functions. Could we please have more examples of different behaviours of the two functions? Is there a case for having both?

@zifuyang
Copy link

i second this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants