]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7a94800) | 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)
commite6454d89343d6ad3195360a0d5a584d5ad3a3575
tree80809d996dc99399d34bd457e59586978265ee48tree | snapshot
parent7a94800f065f001bf08f911ffcec28cea08c2187commit | 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.
components/tactics/paramodulation/equality.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.