기존의 Butterfly는 포기했고 논리 프레임워크를 만들 예정임.


먼저, 상수는 0항 함수로 술어는 Bool로 가는 함수로 볼 수 있음.

또한 함수에 바인더 `[]'를 붙여서 변수를 묶을 수 있음.

인터프리터가 지시 파일을 읽은 다음에야 인터프리터와 대화할 수 있는데,

지시 파일의 일부분을 예로 들어 보겠음.

  1. #language NaturalNumber
  2. Nat ::= succ( Nat ), zero( ).
  3. Bool ::= true( ), false( ).
  4. And( Bool, Bool ) : Bool.
  5. Or( Bool, Bool ) : Bool.
  6. Implies( Bool, Bool ) : Bool.
  7. Iff( Bool, Bool ) : Bool.
  8. Not( Bool ) : Bool.
  9. Bottom( ) : Bool.
  10. All[]( Bool ) : Bool.
  11. Some[]( Bool ) : Bool.
  12. Eq( Nat, Nat ) : Bool.
  13. Plus( Nat, Nat ) : Nat.
  14. Mult( Nat, Nat ) : Nat.
  15. #end

대문자로 시작하고 괄호가 안 붙은 건 타입의 식별자이고,

대문자로 시작하고 괄호가 붙은 건 함수의 식별자이고,

소문자로 시작하고 괄호가 안 붙은 건 생성자의 식별자이고,

소문자로 시작하고 괄호가 붙은 건 변수의 식별자임.

이제 추론 규칙만 작성하면 인터프리터를 증명보조기로 쓸 수 있음.

예를 들어 다음과 같이 말할 수 있음.

"assume) All[x:Nat]( Eq( Plus( x, zero( ) ), x ) )."

"declare) x : Nat."

"all_elimination 1) Eq( Plus( x, zero( ) ), x )."

그런데 추론 규칙을 작성하는 문법을 아직 고안 중임.