Open
Conversation
…straints, improve explanation of free variables in antecedents, fix redundant phrasing in logical axioms, update proof context specification, and enhance LaTeX consistency
…aints for `constrained-proof`, refine GEN and SKO rules with added admissibility considerations, clarify reference system axioms, and improve LaTeX consistency
…or `constrained-proof`, adjust GEN and SKO rules with improved admissibility and logical axiom handling, enhance proof context specification, and improve LaTeX consistency
…fy assignment descriptions, simplify proof transformation explanation, update definitions for improved precision, and enhance LaTeX consistency
…imp`, extend SKO rule logic for multi-variable cases, refactor free variable collection with `StringSet`, and enhance `is_sko_aligned` validation for improved precision and consistency
…d functions for CTV, SKO, and GEN rules, introduce `derive_formula` for shared logic in proof validation, and update rule validation for clarity and consistency
…replacing redundant `name` field with `args` list for improved consistency and clarity in JSON schema
…nd include `json` import to enhance debugging functionality in `kernel.py`
This commit adds a new submodule `repositories/ctxproof` pointing to the ctxproof repository. This enhances project modularity by including the necessary external dependency.
This script initializes OPAM if needed, installs dependencies, and builds the CtxProof project. It also copies the built binary to the target directory for use in the reason project.
…lasses and create ctxproof examples in notebooks
…h` in reason-check pipeline
…grate with kernel logic, and update tests
…ula parsing, implement `extract_formula_from_ctxproof`, refine kernel logic for `prove_tautology`, and enhance `str_to_var` encoding with `isascii` check. Update assets and include extensive tests.
…andling equivalence of quantifier expressions, update `language.py` with examples and integration, and extend tests to cover quantifier equivalence scenarios
…nd new methods (`exists`, `all`) in `ProvedTransformer` for handling quantifier equivalence; update `_transform` to support quantifier cases and extend tests with comprehensive scenarios
…ethods in `ProvedTransformer` for De Morgan transformations on quantifiers; update `neg` to include quantifier cases, integrate `qty_tau` imports, and expand tests with comprehensive scenarios
…proof validation efficiency in `kernel.ml`.
…or proof validation.
…pdate associated logic, and align tests for consistency and simplification.
Introduced a utility function to save ctxproof strings to files, organized in a 'proofs' directory with SHA256-based filenames. Updated the kernel to save proofs when DEBUG is enabled, aiding debugging of both correct and incorrect cases.
…al; optimize Symbol hashing logic
Introduce the PSU (Predicate Substitution) rule, enabling substitution of predicate patterns with formulas while preserving variable scoping. Added unit tests for PSU and related substitution functionality to ensure correctness and prevent edge case errors like variable capture.
Replaces `Assumption`, `Axiom`, `Rule`, and `Block` with a unified `Statement` base class to streamline inheritance and parent-child relationships. Removes unused code and comments for better readability and maintainability, simplifying the implementation.
Introduced dynamic index computation in `Ref` with parent chain traversal, improving flexibility in reference handling. Enhanced Skolem constant replacement to reflect updated indices and integrated these changes into TPTP formula conversions. Adjusted statement handling logic in `Block` and enabled more robust `Ref` linking.
Moved `formula_to_tptp` to handle generic formulas and created `formula_of_statement_to_tptp` for statement-specific processing. Simplified and standardized TPTP conversion method calls across various `to_ctxproof` implementations. Removed unused `get_next_ref` method to enhance code clarity and maintainability.
Disabled DEBUG mode in the proofkit kernel's initialization file to prevent unnecessary debugging output. This change ensures a cleaner production environment.
Replaced the custom skolem replacement logic with a dedicated `SkolemReplacer` class extending `Transformer`, improving modularity and readability. Simplified core Transformer methods to return results directly, enhancing code maintainability.
The `from_json` and `jsonize` modules, along with related `to_json` methods in the `proof.py` classes, have been deleted. This streamlines the code by removing unused or unnecessary JSON handling features.
Introduced a `schema` method with caching for improved performance and added a `prepend` method to efficiently insert statements at the beginning of a `Block`. Updated testing and notebooks to utilize the schema mechanism and validate functionality.
Refactored schema handling by introducing `lang()` and updating `schema` method usage across proofkit modules. Enhanced language initialization logic in proof kernel for better default handling. Adjusted notebooks and rules to align with schema mechanism updates. Enabled DEBUG mode for development purposes.
Replaced direct `schema` and `PSU` calls with the `schema_with_result` helper function across proofkit modules. This change simplifies schema usage, reduces boilerplate code, and improves readability without altering existing functionality.
…pendency Replaced all `schema_with_result` calls with direct function calls in various proofkit modules, introducing the `@sub_schema` decorator for encapsulating schema transformations. Simplified proofs by removing redundant boilerplate, aligning with recent schema handling improvements, and enhancing code readability.
Added @sub_schema decorators for schema functions, updated proof management to allow finer control over statement indices, and introduced support for $true and $false in TPTP predicates. Commented or modified several tests and sections for consistency and debugging purposes.
…utilities Replaced direct `Predicate(TRUE/FALSE)` instances with `TruePred` and `FalsePred` helper functions for consistency and modularity. Updated proof kernel, TPTP parser, and FOF operations accordingly, simplifying logic connective and quantifier handling.
…agement Applied `@sub_schema` decorators to multiple schema functions across `qty_tau.py` and `tautologies.py`, aligning with recent schema handling conventions. Updated proof management in `proof.py` to handle statement indices more precisely, improving schema execution. Adjusted `ctxproof.py` for testing consistency.
Introduce `SUB_SCHEMA_ACTIVE` flag to toggle schema behavior, ensuring flexibility in function returns. Add `NnfProvedTransformer` to manipulate formulas in the notebook, showcasing an example transformation and adjusting output context proof.
Disabled tests related to variable capture errors, including `test_variable_capture_prevention` and `test_capture_check_with_quantified_replacement`. These tests are now commented out for potential future debugging or adjustments.
This commit updates the `foundation` repository, but the diff does not detail any specific changes made. Further context or inspection may be needed to understand the exact modifications.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.