Age | Commit message (Collapse) | Author |
|
Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.
|
|
Implementation of the translation of a number of rules that follow the clause pattern into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of AND_ELIM rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of CONTRA rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of MODUS_PONENS rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of SPLIT rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of FACTORING rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Provides background on the translation into the Alethe calculus that is common to all rules.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
|
|
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled.
During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.
|
|
Implementation of the translation of SCOPE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of the translation of ASSUME rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
|
|
Added proof postprocessor class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Added final callback class to alethe_proof_processor header file.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Added alethe_proof_processor header file and introduced callback class.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
Implementation file for Alethe proof rules.
|
|
Adds header for Alethe proof rules
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|