Activity
DRuleParser::compressAbstractDProof(): remove test code
DRuleParser::compressAbstractDProof(): remove test code
Force push
DRuleParser::compressAbstractDProof(): remove test code
DRuleParser::compressAbstractDProof(): remove test code
fix purifier: synchronized modifications of std::map
fix purifier: synchronized modifications of std::map
found shorter proofs via new '--transform -x' proof compression feature
found shorter proofs via new '--transform -x' proof compression feature
experimental support of synthesizing proof compression: '--transform -x'
experimental support of synthesizing proof compression: '--transform -x'
Force push
experimental support of synthesizing proof compression: '--transform -x'
experimental support of synthesizing proof compression: '--transform -x'
fix crash on '--assess' when relevant !.def file has empty removals list
fix crash on '--assess' when relevant !.def file has empty removals list
readme: clarify different notions of proof minimality
readme: clarify different notions of proof minimality
add '--transform -w' and '--unfold -v': read input without conclusions
add '--transform -w' and '--unfold -v': read input without conclusions
link to mirror repository at codeberg.org/xamidi/pmGenerator in readme
link to mirror repository at codeberg.org/xamidi/pmGenerator in readme
Force push
link to mirror repository at codeberg.org/xamidi/pmGenerator in readme
link to mirror repository at codeberg.org/xamidi/pmGenerator in readme
Force push
link to mirror on codeberg.org in readme, remove helper tools' code
link to mirror on codeberg.org in readme, remove helper tools' code
found 19 shorter proofs for minimal 1-base proof minimization challenge
found 19 shorter proofs for minimal 1-base proof minimization challenge
add time measurements to proof compression output
add time measurements to proof compression output
--extract -z: force redundant schema removal for '-t'
--extract -z: force redundant schema removal for '-t'
'--transform -b -e' fix: unfold correct rules in case they were shifted
'--transform -b -e' fix: unfold correct rules in case they were shifted
--transform -b: duplicate conclusion removal via subproof replacements
--transform -b: duplicate conclusion removal via subproof replacements
proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'
proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'
Force push
proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'
proof collection: make '-g -b' the default and rename '-g -v' to '-g -b'
allow redundant references in proof summaries to be parsed
allow redundant references in proof summaries to be parsed
make '--transform -z' multi-threaded (with single-threaded option)
make '--transform -z' multi-threaded (with single-threaded option)
custom tools ./formulasFromSummaries and ./uniteLists
custom tools ./formulasFromSummaries and ./uniteLists
--assess: feature to assist with assessments of generation expenditures
--assess: feature to assist with assessments of generation expenditures
-g: precise iteration limit calculations for timing estimations
-g: precise iteration limit calculations for timing estimations
filter out duplicate abstract summary indices (in case of redundancies)
filter out duplicate abstract summary indices (in case of redundancies)