구내 순서

Question

규칙에서 구내 순서를 변경하는 방법은 무엇입니까?

mp: ?P ⟶ ?Q ⟹ ?P ⟹ ?Q 

우리가 순서를 변경할 수 있습니다 : 이자벨의 천연 공제 규칙에 예를 들어 ,

?P ⟹ ?P ⟶ ?Q ⟹ ?Q 

나는 rev_mp을 사용하거나 새 보조 정리를 정의하지만 내가 찾던 여부가 있습니다 전제의 순서를 변경하는 정리 수정 자입니다.

Answer 1

정리의 전제는 rotated 속성으로 회전 할 수 있습니다. 회전 할 건물의 수를 지정할 수도 있습니다 (예 : mp[rotated 1]). AFAIK에는 건물을 임의로 치환하는 속성이 없습니다.