anthem 1.0.0 Beta 4

This is a preview release of anthem 1.0.0, which implements a new mode to verify that tight logic programs implement first-order-logic specifications according to our ICLP 2020 publication Verifying Tight Logic Programs with anthem and Vampire (Jorge Fandinno, Vladimir Lifschitz, Patrick Lühne, and Torsten Schaub).

Features

• new command anthem verify-program to verify tight logic programs against first-order-logic specifications

Known Issues

• the previous anthem mode for verifying the strong equivalence of logic programs is currently unavailable and will be brought back at a later date (for now, use anthem 0.2 for verifying the strong equivalence of logic programs)
• Vampire search options not yet configurable
• minor parser issues (for example, missing absolute value function)

anthem 0.2.0 RC 4

Changes

• new translation mode for proving strong equivalence via logic of here-and-there (--mode=here-and-there, enabled by default)
• former completion-oriented translation scheme now available with --mode=completion

Features

• new TPTP output format for usage with theorem provers (--output-format=tptp, while --output-format=human-readable is the default)
• full support for both integer and symbolic values with additional transformation for TPTP output
• new option to enforce this transformation in the human-readable output format as well (--map-to-integers=always, while the default, --map-to-integers=auto, only applies the mapping for TPTP output)
• information note if the input program is definite or not

Bug Fixes

• omits unnecessary parentheses around function and predicate arguments

anthem 0.1.9

Changes

• turns on completion and simplification by default, which can now be switched off with --no-complete and --no-simplify

Features

• detection of integer variables and integer predicate parameters
• command-line option --no-detect-integers to disable integer variable detection
• new simplification rule applying to integer variables
• support for declaring functions integer with the #external directive

Bug Fixes

• fixes incorrect translation of unsupported choice rules with multiple elements by returning an error instead
• fixes precedence of intervals by enclosing them in parentheses

Checksums

anthem-0.1.9-linux-x86_64.tar.gz

algorithm	checksum
MD5	d1789465a4eaddf6ed6ac55d526a9fa9
SHA-256	4afd5f2e87fc1c0bc6a7c1fb2eb69256bc7708bb544b0be7468423ce99f25d41
SHA-512	d61993979106e65ff19d328f6aef0f082193a7277f980eb076ab769c094ace8643f98d00e4176d30e3065a10510493ded81ec3fb72cebe716f17a5e1b7b35037

anthem 0.1.9 RC 5

Features

• optional detection of integer variables and integer predicate parameters
• command-line option --detect-integers to enable integer variable detection
• support for declaring functions integer with the #external directive
• new simplification rule applying to integer variables

Checksums

anthem-0.1.9-rc.5-linux-x86_64.tar.gz

algorithm	checksum
MD5	65c037946c367cc3df1419bf708a4112
SHA-256	cc8cfa8f1150944ccc0eae2d40d72eb0ebb4d28171f17d7c9a72dcb83e0eafa9
SHA-512	c5cf2afffc4a9e38b378ac739d3f7e658fe83a4ebf613eab3a9ed91a333f3643cc863a9dbab0bdbefb375109b2dac95e0f558565281de842e01385f703d1b095

anthem 0.1.8

Features

• more and advanced simplification rules
• adds support for exponentiation (power) and modulus (absolute value)
• new examples: prime numbers, permutation generator, and graph coloring (extended)

Checksums

anthem-0.1.8-linux-x86_64.tar.gz

algorithm	checksum
MD5	3cca75baf4fbe7b2cb33b912a29071fc
SHA-256	e1f586978d8f86a8a28fcd850fb92a6d0807c4af84323d902e9ed61e19673b22
SHA-512	f0b4318bd935e5a6112b1f44831761d86cfbb3c5be7641224ecbd7131db13c388f56ce0285710d68e78bc9d7e888a0870a8185b1168ad0d052ff6c7659954e82

anthem 0.1.7

Features

• support for declaring placeholders with the #external directive

Internal

• drops Boost dependency in favor of the header-only command-line option library cxxopts

Checksums

anthem-0.1.7-linux-x86_64.tar.gz

algorithm	checksum
MD5	af6c17edc63222f43652bd1a27a5038b
SHA-256	4636abe63c7b80da7b61d2b9914bb75d92705bc7f0beeda8920d1fd9cb6566f8
SHA-512	c32363fa88c63ee4b7e17dc883c4dee667d35c480e381eae9639f6d5f338e527140f230076c50212e01f1d0dd532c6706be0c2547ed4918a46edce5c17c08c66

anthem 0.1.6

Features

• unique IDs for all variables (user-defined variables are renamed)
• support for hiding predicates from completed output by using #show statements
• more simplification rules with --simplify
• command-line option --parentheses to fully parenthesize the output
• adds multiple example instances for experimenting

Bug Fixes

• adds missing error message when attempting to read inaccessible file
• removes unnecessary parentheses after simplification
• fixes incorrect simplification with binary operations in arguments

anthem 0.1.5

Bug Fixes

• fixes lost signs with negated 0-ary predicates

anthem 0.1.4

Features

• completion of input programs (optional)
• command-line option --complete to turn on completion

anthem 0.1.3

Features

• support for anonymous variables

Bug Fixes

• fixes incorrectly simplified rules with comparisons
• fixes misleading error message concerning negated, unsupported body literals