-
Notifications
You must be signed in to change notification settings - Fork 0
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
upstream: convert oracle and checker work into Lean and Aristotle contributions
documentationImprovements or additions to documentationImprovements or additions to documentationenhancementNew feature or requestNew feature or requestproofProof objects, checkers, or formalizationProof objects, checkers, or formalizationStatus: Open.#6 In SMC17/logic-zig;exhibit: complete modal K, T, S4, and S5 decision procedures
exhibitExecutable museum exhibit workExecutable museum exhibit workneeds-specificationFormal identity or completeness contract is incompleteFormal identity or completeness contract is incompleteproofProof objects, checkers, or formalizationProof objects, checkers, or formalizationStatus: Open.#5 In SMC17/logic-zig;correctness: carry ranked countermodels for failed KLM queries
correctnessSoundness, completeness, model, proof, or certificate correctnessSoundness, completeness, model, proof, or certificate correctnessexhibitExecutable museum exhibit workExecutable museum exhibit workproofProof objects, checkers, or formalizationProof objects, checkers, or formalizationStatus: Open.#4 In SMC17/logic-zig;proof: generate Lean-to-Zig finite-matrix differential fixtures
correctnessSoundness, completeness, model, proof, or certificate correctnessSoundness, completeness, model, proof, or certificate correctnessenhancementNew feature or requestNew feature or requestproofProof objects, checkers, or formalizationProof objects, checkers, or formalizationStatus: Open.#3 In SMC17/logic-zig;- Status: Open.#1 In SMC17/logic-zig;