anthem 1

축가

답안 세트 프로그램을 1차 정리 증명 언어로 변환

이 프로젝트의 상태

메모

현재 Patrick Lühne이 제작했으며 더 이상 개발되지 않는 anthem 버전 1을 보고 계십니다. 이 저장소에 대한 추가 커밋은 이루어지지 않습니다.

최신 버전의 Anthem에 관심이 있다면 새로운 저장소를 살펴보세요.

개요

anthem ASP 프로그램( clingo 입력 언어)을 Prover9와 같은 1차 정리 증명자의 언어로 변환합니다.

용법

프로그램이 사양을 구현하는지 확인하려면 verify-program 명령을 사용하여 anthem 호출하세요.

 $ anthem verify-program <프로그램 파일> <사양 파일>...

여러 사양 파일을 지정할 수 있습니다. 이는 가정과 사양에서 기본형과 공리를 분리하는 데 유용합니다.

숫자의 제곱근의 바닥을 계산하는 예는 다음과 같이 재현할 수 있습니다.

 $ anthem 확인 프로그램 예제/example-2.{lp,spec,lemmas}

중괄호 표기법은 Bash의 약어입니다.

 $ anthem 검증 프로그램 예제/example-2.lp 예제/example-2.spec 예제/example-2.lemmas

기본적으로 anthem 번역된 수식에 대해 Clark의 완성을 수행하고, 어떤 변수가 정수인지 감지하고, 몇 가지 기본 변환 규칙을 적용하여 출력을 단순화합니다.

--no-complete , --no-simplify 및 --no-detect-integers 옵션을 사용하여 이러한 처리 단계를 끌 수 있습니다.

건물

anthem Rust의 cargo 툴체인으로 제작되었습니다. Rust를 설치한 후 다음과 같이 anthem 빌드할 수 있습니다.

 $ 자식 클론 https://github.com/potassco/anthem.git
$ CD 찬가
$ 화물 빌드 --릴리스

그러면 anthem 바이너리가 target/release/ 디렉터리에서 사용 가능해집니다. 또는 다음과 같이 cargo 사용하여 anthem 호출할 수 있습니다.

 $ 화물 실행 -- verify-program <프로그램 파일> <사양 파일>...

기여자

• 패트릭 뤼네