이는 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 명령 증명9입니다.
프로그램:
이름
prover9 - 해상도/패러모듈레이션 정리 증명자
개요
잠언 9 [옵션] 입력 파일 > 결과물 파일
잠언 9 [옵션] -NS 입력 파일 > 결과물 파일
기술
이 매뉴얼 페이지는 간략하게 설명합니다 잠언 9 명령.
잠언 9 XNUMX차 및 등식 논리에 대한 자동화된 정리 증명기입니다. 이것은
의 후계자 수달(1) 증명자. 잠언 9 순서의 추론 기술을 사용합니다.
리터럴 선택을 통한 해상도 및 파라모듈레이션.
옵션
아래에 옵션 요약이 포함되어 있습니다.
-h 명령줄 옵션 목록을 봅니다.
-x 실험적으로 향상된 자동 모드를 활성화합니다. 자세한 내용은
잠언 9 수동.
-p 출력을 완전히 괄호로 묶습니다.
-t n 지속할 수 있도록 검색 제한 n 초. UNIX 계열 시스템의 경우 `user
CPU' 시간이 사용됩니다.
-f 파일
에서 입력 받기 파일 표준 입력 대신.
onworks.net 서비스를 사용하여 온라인에서 prover9 사용
