변화에 의한 통일

Question

나는 글을 쓰고 있다 통일 다음과 함께 사용하기 위한 F#의 알고리즘 AST 다음을 사용하여 변환 "용어 재작성 및 그 모든 것" (월드캣) 프란츠 바더(Franz Baader)와 토비아스 닙코우(Tobias Nipkow)가 지음.섹션 4.6 변환에 의한 통합의 경우 예제가 포함된 수학 이론이 너무 많았고 원하는 만큼 명확하지 않았습니다.

누군가 변환을 활용하는 더 간단한 예를 제시하거나 지적할 수 있습니까?

삭제, 분해, 방향 지정, 제거.

Answer 1

삭제: t = t 무의미하며 방정식 세트에서 제거될 수 있습니다.

1 =? 1 -> nil

동양:우리는 모든 방정식을 다음과 같은 형태로 원합니다. x =? t, 따라서 다음과 같은 형태로 방정식을 뒤집습니다. t =? x.

2 =? x1 -> x1 =? 2

제거하다:주어진 x =? t, 다른 모든 방정식을 변경하여 x ~와 함께 t.

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

분해:다음과 같은 형태의 방정식을 얻으려면 함수를 취하고 제거해야 합니다. x =? t.이 프로세스는 기술적으로 한 번에 하나의 기능만 제거한다는 점에 유의하십시오.

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

이것이 도움이 되기를 바랍니다.