coq-library-undecidability
coq-library-undecidability copied to clipboard
uds-psl
A library of mechanised undecidability proofs in the Coq proof assistant.
Currently, our coqdoc is a complete mess. I don't know how to fix this in a good way, and it's well possible that we want to ignore the issue for...
After discussion with Andrej, here's a proposal how to structure the repository in the future in order to be most easily to maintain. Please add your thoughts from a user...
Andrej's investigation into performance yielded that we shouldn't use `Print Assumptions`, because it is too slow. Now an open question is whether we want `Check` commands after important theorems or...
Regarding the naming definition we started in #41, I did some (limited) research what standard resources call "recursively enumerable". (My opinion then follows below) Rogers: > **Definition** A is recursively...
As previously discussed with @yforster, this PR replaces the laborious, direct `L_computable -> TM_computable` proof by a shorter `L_computable -> MMA_computable`, `MMA_computable -> TM_computable` variant with several benefits. - no...
This PR is a first step towards a proof of undecidability of Wang tilings with a fixed origin (ie tiling the North-East part of the plane). The intended reduction chain...
- added higher-order matching wrt. beta-equivalence `HOMbeta` - added reduction from `SSTS01` to `HOMbeta` resulting in `undecidable HOMbeta` The reduction is quite different from the known technique by Loader [1]....
To enable easier reuse of this library, please consider changing its license to a permissive license like [MIT](https://spdx.org/licenses/MIT.html) or a weak copyleft license like [MPL-2.0](https://spdx.org/licenses/MPL-2.0.html). The issue with strong copyleft...
In the current version of the library, inversion on formulas is not working as expected. In some cases, for instance, `congruence` falls short of closing a goal `s = t`...
