]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0034d87) | patch
Experimental: cycles in proofs generated by paramodulation are now detected
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 6 Dec 2006 15:54:39 +0000 (15:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 6 Dec 2006 15:54:39 +0000 (15:54 +0000)
commitcca52355d183a00695b9e310b17c8945ae915b64
tree6498a91560e625e24d5867f4e9c61e65c8bb2215tree | snapshot
parent0034d878cbd23062c7312e13d654ac7fd23a01cfcommit | diff
Experimental: cycles in proofs generated by paramodulation are now detected
and removed.
However, letins that become useless after this operation are not simplified.
Simplifying them (when they became linear) could introduce more cycles that
require a second simplification and so on.
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.