summaryrefslogtreecommitdiff
path: root/src/proof/alethe
AgeCommit message (Collapse)Author
2021-10-26[proofs] Modularize check for whether a clause is singleton (#7497)Haniel Barbosa
Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.
2021-10-26[proofs] Alethe: Translate Block of clause pattern rule (#7406)Lachnitt
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>
2021-10-26[proofs] Alethe: Translate AND_INTRO rule (#7405)Lachnitt
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate AND_ELIM rule (#7404)Lachnitt
Implementation of the translation of AND_ELIM rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate CONTRA rule (#7403)Lachnitt
Implementation of the translation of CONTRA rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)Lachnitt
Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-25[proofs] Alethe: Translate MODUS_PONENS rule (#7401)Lachnitt
Implementation of the translation of MODUS_PONENS rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-25[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)Lachnitt
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-25[proofs] Alethe: Translate SPLIT rule (#7399)Lachnitt
Implementation of the translation of SPLIT rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-22[proofs] Alethe: Translate FACTORING rule (#7398)Lachnitt
Implementation of the translation of FACTORING rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-22[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)Lachnitt
Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-20[proofs] Alethe: Documentation on Translation (#7394)Lachnitt
Provides background on the translation into the Alethe calculus that is common to all rules. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-23[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)Lachnitt
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
2021-09-23[proofs] Alethe: Translate THEORY_REWRITE (#7236)Lachnitt
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
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.
2021-09-23[proofs] Alethe: Translate SCOPE rule (#7224)Lachnitt
Implementation of the translation of SCOPE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-21[Proofs] Alethe: Translate ASSUME rule (#7213)Lachnitt
Implementation of the translation of ASSUME rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-21[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)Lachnitt
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>
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
2021-09-17[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)Lachnitt
Added proof postprocessor class to alethe_proof_processor header file. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-17[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)Lachnitt
Added final callback class to alethe_proof_processor header file. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-15[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)Lachnitt
Added alethe_proof_processor header file and introduced callback class. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-15[proof] Added printer for proof rule names (#7185)Lachnitt
Implementation file for Alethe proof rules.
2021-09-15[proof] Alethe proof rules (#7180)Lachnitt
Adds header for Alethe proof rules Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback