이사플랜너
IsaPlanner |
이사플랜너는[1] 인터랙티브 증명비서 이사벨의 증명기획자다.원래 루카스 딕슨이[2] 에든버러 대학에서 박사학위 논문의 일부로 개발한 이 논문은 현재 에든버러에서 정보학을 전공하는 수학 추리 그룹의 회원들에 의해 유지되고 있다.이사 플랜너는 에든버러에서 작성된 일련의 증명 계획자들 중 가장 최근의 것이다.초기 기획자들은 Clam과 LambdaClam을 포함한다.
특징들
IsaPlanner는 사용자가 이론들을 추측하고 증명하기 위해 결합기 언어를 사용하여 추론 기법을 인코딩할 수 있도록 한다.IsaPlanner는 추리 상태, 공개 목표 기록, 현재 증명 계획 및 기타 중요한 정보를 조작하여 작업하며, 결합자는 추리 상태를 후임 추리 상태의 게으른 목록에 매핑하는 기능이다.
이사플랜너의 도서관은 분기 및 반복을 위한 결합기를 다른 작업 중에서도 공급하고 있으며, 이러한 결합기와 단순한 추론 기법을 결합하여 강력한 추론 기법을 만들 수 있다.
몇 가지 추론 기법이 IsaPlanner 내에서 구현될 수 있으며, 특히, IsaPlanner는 동적 잔물결 구현, 고차적 환경에서 작업할 수 있는 잔물결 경험적 경험적 경험적 경험적 경험, 유도에 의한 증거에 대한 추론적 기법을 특징으로 한다.
추가 기능에는 증명 시도를 수동으로 단계별로 진행하는 인터랙티브 추적 도구와 계층적 증거를 보고 조작하는 모듈이 포함된다.
계획된 기능
증거들은 비평가들의 기능 currently[언제?],, 미래에 계획되어 지고 향상된 세트 더 고차원적 영역에서 사용하기에 적합한, 역동적인 관계형 물놀이를, 잔물결 소리를 내며 흐르는 관계는 표현으로 기능적 표정, 다시 더 높은 순서 도메인에 사용하기에 적합하고 integrat에 반대해 잔물결이 이에 적합한 발견적.의 이온증명 일반과 함께 이사 플랜너.[citation needed]
