Replace variables in MGU properly

This commit is contained in:
Arne Keller 2021-07-02 15:13:10 +02:00
parent 480275e3a7
commit 116aea51c3

View File

@ -133,6 +133,7 @@ public class Tree implements TermVisitorTree {
Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions); Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions);
Type assType = typeVarFactory.nextTypeVariable(); Type assType = typeVarFactory.nextTypeVariable();
TypeAbstraction assAbs = new TypeAbstraction(assType); TypeAbstraction assAbs = new TypeAbstraction(assType);
extendedTypeAssumptions.remove(absTerm.getVariable());
extendedTypeAssumptions.put(absTerm.getVariable(), assAbs); extendedTypeAssumptions.put(absTerm.getVariable(), assAbs);
Type premiseType = typeVarFactory.nextTypeVariable(); Type premiseType = typeVarFactory.nextTypeVariable();