-
Notifications
You must be signed in to change notification settings - Fork 6
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Better Proof Structure
kind:enhancementNew feature or upgrade of a previous oneNew feature or upgrade of a previous onepart:proof-searchThe PR is about the proof-search algorithmThe PR is about the proof-search algorithmStatus: Open.Applying the substitution to a twin makes the proof output incorrect
kind:bugSomething isn't workingSomething isn't workingpart:proof-outputAbout the vanilla proof output (in custom format)About the vanilla proof output (in custom format)part:proof-searchThe PR is about the proof-search algorithmThe PR is about the proof-search algorithmStatus: Open.Unsoundness in seemingly easy problem
kind:inconsistencyGoéland is unsoundGoéland is unsoundpart:proof-searchThe PR is about the proof-search algorithmThe PR is about the proof-search algorithmStatus: Open.Unsoudness on a bunch of problems in equality reasoning
kind:inconsistencyGoéland is unsoundGoéland is unsoundStatus: Open.Error when waiting for children - substitution is not empty but children close by themselves
kind:bugSomething isn't workingSomething isn't workingpart:proof-searchThe PR is about the proof-search algorithmThe PR is about the proof-search algorithmStatus: Open.#58 In GoelandProver/Goeland;Infinite loop in EliminateMeta with seemingly unrelated option
kind:bugSomething isn't workingSomething isn't workingpart:proof-outputAbout the vanilla proof output (in custom format)About the vanilla proof output (in custom format)Status: Open.#56 In GoelandProver/Goeland;Having debug levels
kind:requestRequesting a new featureRequesting a new featurepart:loggingThe PR/issue is about loggingThe PR/issue is about loggingStatus: Open.#25 In GoelandProver/Goeland;GS3 failure: tried to apply a missing hypothesis when using
-innerand-preinnerflagskind:bugSomething isn't workingSomething isn't workingpart:pluginsThe PR is about plugin-related codeThe PR is about plugin-related codeStatus: Open.Failure of unit tests
kind:bugSomething isn't workingSomething isn't workingpart:unit-testsThe PR is about unit testingThe PR is about unit testingStatus: Open.#13 In GoelandProver/Goeland;