thf를 통해 객체 논리를 만드는 방법

Isabelle에서 객체 논리를 어떻게 만들 수 있습니까? 나는이 문서에서 개체의 논리를 만드는 방법에 대해 발견 무엇thf를 통해 객체 논리를 만드는 방법

는 이자벨/ISAR 참조 설명서에서

2.3 Example: First-Order Logic

했다.

특히 객체 논리를 읽고 특히 무엇을 사용해야합니까?

THF 용지 짧은 대답은 here

2013-06-10 Gergely

자세히 설명해주세요. thf는 무엇인가요? –

나는 너의 목표를 꽤 얻지 못한다. 분명히 해줄 수 있니? – chris

오브젝트 로직을 작성하는 전통적인 방법은 Pure에서 인코딩을 작성하는 것입니다. 나는 이제 이것이 THF를 사용하여 가능하다고 들었다. 문제는 어떻게? – Gergely

같이 높은 주문 양식을 입력 할 때 : 현재, 당신은 할 수 없습니다.

Isabelle에는 THF를 통해서만 오브젝트 논리를 정의 할 수있는 기능이 없습니다. 네가 인용 한 예제에서와 같이 객체 논리는 여전히 순수한 건물로 정의되어있다.

2013-06-22 03:41:35 lsf37

답변