anthem 1

hino

Traduzir programas de conjunto de respostas para linguagem de prova de teoremas de primeira ordem

Status deste projeto

Observação

No momento, você está vendo a versão 1 do anthem , que foi construída por Patrick Lühne e não está mais em desenvolvimento. Nenhum outro commit neste repositório será feito.

Se você estiver interessado em uma versão recente do hino, dê uma olhada no novo repositório.

Visão geral

anthem traduz programas ASP (na linguagem de entrada clingo ) para a linguagem de provadores de teoremas de primeira ordem, como Prover9.

Uso

Para verificar se um programa implementa uma especificação, invoque anthem usando o comando verify-program :

 $ anthem verify-program <arquivo de programa> <arquivo de especificação>...

Observe que vários arquivos de especificação podem ser especificados. Isso é útil para separar lemas e axiomas de suposições e especificações.

O exemplo para calcular o valor mínimo da raiz quadrada de um número pode ser reproduzido da seguinte forma:

 $ exemplos de programas de verificação de hino/exemplo-2.{lp,spec,lemas}

A notação de colchetes é uma abreviação do Bash para

 $ hino verificar-programa exemplos/exemplo-2.lp exemplos/exemplo-2.spec exemplos/exemplo-2.lemmas

Por padrão, anthem realiza a conclusão de Clark nas fórmulas traduzidas, detecta quais variáveis ​​são inteiras e simplifica a saída aplicando várias regras básicas de transformação.

Essas etapas de processamento podem ser desativadas com as opções --no-complete , --no-simplify e --no-detect-integers .

Prédio

anthem é construído com o conjunto de ferramentas cargo do Rust. Depois de instalar o Rust, anthem pode ser construído da seguinte forma:

 $ git clone https://github.com/potassco/anthem.git
$ cd hino
$ construção de carga --release

O binário anthem estará então disponível no diretório target/release/ . Alternativamente, anthem pode ser invocado usando cargo da seguinte maneira:

 $ cargo run -- verify-program <arquivo de programa> <arquivo de especificação>...

Colaboradores

• Patrick Luhne