potassco / anthem Goto Github PK

The TPTP formatter currently prints f__integer__(1) = f__integer(1) instead of 1 = 1.
This is also true for other relation, e.g. p__less__(f__integer__(1), f__integer__(2) instead of $less(1,2).

ASP comments are preceded by %
Spec language comments could also be defined as such

It seems that your program doesn’t like sqrt_b as a predicate name in a program

The split function passes an interior formula to split_implication, removing the outermost quantification. This can be fixed for constraints by re-quantifying all free variables at the final step.

A user guide should not contain any annotated formulas other than

role: assumption
direction: universal

Otherwise an error should be thrown.

If any function constants other than placeholders occur in the formulas of a user guide, specification, or proof outline, a warning should be issued.

Write formatters for pretty printing the AST.
E.g., use https://docs.rs/pretty/latest/pretty/.

I want to write

program.
    .tau_star()
    .gamma()

instead of

gamma(tau_star(program))

anthem translate should read its input from stdin if <INPUT> is not given as an argument. This allows constructions like anthem translate --with tau-star <INPUT> | anthem translate --with gamma.

Symbolic constants should be of type "symbol" not "object"
Add a "symbol" custom type to preamble rather than relying on native $i sort

From "Verifying Tight Logic Programs with Anthem and Vampire":
"A program is a finite set of rules."
"For any program Π, τ ∗Π stands for the set of formulas τ ∗R for all rules R of Π."
And a collection of closed logical formulae is a theory, so an ASP Program node should translate to a FOL Theory node.

Placeholders are syntactically indistinguishable from symbolic constants, but semantically they behave like free variables. Since TPTP requires type-casting for comparisons, e.g.

$lesseq(a, n)

is forbidden if a is a function constant but n is an integer placeholder, this makes formatting them correctly in TPTP very inconvenient. Currently using a temporary rename-and-replace strategy with regexes as a post-processing step in zach/dev.

One option is to make placeholders part of the fol AST: general-sorted placeholders are treated similarly to symbolic constants and integer-sorted placeholders are treated similarly to integer terms. So, rather than replacing them with variables of the appropriate sort, we could replace them with zero-arity functions of the appropriate sort.

Ultimately, I'm not sure there is a perfect way to do this. Parsing and formatting should be context-independent, but the presence of a user guide affects whether n is treated as a symbolic constant, a free-valued integer function, or a free valued general function.

VL requested (Feb 2, 2024) that the convention of writing "N$i" to denote an integer variable named N be converted to just "N$".

A way to write variables with sort information is:

N$g is understood as a general-sorted variable named N
N is understood as a general-sorted variable named N

N$i is understood as a integer-sorted variable named N
N$ is understood as a integer-sorted variable named N

For any other sort s, N$s denotes an s-sorted variable named N

Clingo's definition of division/modulo differs from mathematical definition presented in "Verifying Tight Logic Programs with ANTHEM and VAMPIRE" in the case of negative divisors (uses truncation to zero instead of floor).

Up-to-date definitions are in Jorge & Vladimir's "Omega-Completeness..." draft, which adds absolute value as a function to mini-GRINGO and the two-sorted target language.

So do we want to make anthem clingo-compliant and add this?
omega.pdf

The formula

exists I J ( forall I ( p(I) -> q(J) ) & q(I) )

is correct. But it would be easier to read if it were

exists I J ( forall I1 ( p(I1) -> q(J) ) & q(I) )

The FOL parser is unable to parse atoms that begin with "g" for unknown reasons.

For example, "not g" does not parse correctly. In zach/tau_star_v1 branch, see the parse_formula tests in src/parsing/fol/pest.rs for an example, and the tau_star_test16 in tau_star.rs for another example (note that it differs from tau_star_test15 in exactly one character, "g" vs "t" in the atom).

Default formatting should be the inverse of default parsing.

For example, a -> b -> c is equivalent to a -> (b -> c). Should we format those parentheses for clarity?

I should be possible to cascade multiple translations in anthem translate, e.g.

anthem translate --with tau-star, gamma <INPUT>.

This issue is difficult as it requires some kind of dynamic typing with the command line.

The parser is unable to parse the rule

p :- a != b.

Since a is recognized as a predicate before being recognized as a term within a comparison.

Throw unreachable! errors instead of handling SymbolicTerm::Variables in tau*

Parsing error occurs if a file begins with a new line or as such:

% Comment
program

Currently the parser fails the following test case, and throws an error when attempting to parse "n > 1" as a FOL formula.
(
"n > 1",
Formula::AtomicFormula(AtomicFormula::Comparison(Comparison {
term: GeneralTerm::Symbol("n".to_string()),
guards: vec![Guard {
relation: Relation::Greater,
term: GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm(
BasicIntegerTerm::Numeral(1),
)),
}],
})),
)

Show total time required to execute "translate" or "verify" etc.

Currently, the parser doesn't pinpoint where the error actually occurs, and gives a somewhat cryptic "expected EOI" error message for a line containing a syntax error. For example:

      Error: could not parse file `test.lp`
      
      Caused by:
           --> 2:1
            |
          2 | composite(I*J) :- sqrt_b(M), I = 2..M, J = 2..b. 
            | ^---
            |
            = expected EOI

In this case, the parsing error was caused by the "_" in sqrt_b, but the error message doesn't help a user pinpoint that.

Currently the FOL grammar supports parsing and formatting everything up to and including theories. But we still need annotations for these formulas when we parse Anthem specifications or Anthem-P2P user guides. The following grammar rules should be added:

predicate_signature = @{ predicate_symbol ~ "/" ~ (("0") | (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*)) }

statement = { assumption | axiom | spec | lemma | input | output }
assumption = { "assume:" ~ formula ~ "." }
axiom = { "axiom:" ~ formula ~ "." }
spec = { "spec:" ~ formula ~ "." }
lemma = { "lemma:" ~ formula ~ "." }
input = { "input:" ~ (placeholder | predicate_signature) ~ ("," ~ (placeholder | predicate_signature))* ~ "." }
output = { "output:" ~ (predicate_signature) ~ ("," ~ (predicate_signature))* ~ "." }

specification = _{ SOI ~ statement* ~ EOI }

The spec language lets users write formulas like

forall X exists X$i q(X, X$i)

which in TPTP would currently be formatted ambiguously as

![X : $object] ( ?[X : $int]: ( q(X, X) ) )

which Vampire views as a syntax error. Instead, when formatting a variable named X with sort s in TPTP we should print Xs:

![Xg : $object] ( ?[Xi : $int]: ( q(Xg, Xi) ) )

It should be possible to specify the used formatter in anthem translate, e.g.

• anthem translate --with tau-star --format default
• anthem translate --with tau-star --format tptp
• anthem translate --with tau-star --format debug

Feature request from Vladimir. Implementing for sequential proof search should be simple, parallel proof search not so much.

*analysing
    tightness

command_line

convenience
    apply
    unbox

formatting      -> Format structs
    asp
        default
    fol
        default
        tptp

parsing         -> Parser trait
    asp
        pest
    fol
        pest

*verifying
    task        -> Task trait
    problem     -> Problem struct
    proof

simplifiying
    fol
        ht
        *classic

syntax_tree     -> Node trait
    asp
    fol

translating
    gamma
    tau_star
    *completion

Modules marked with an * do not yet exist.
The module problem_building should be renamed into verifying/problem.

We should schedule a group meeting with all Anthem group members to discuss three related issues:

1. Project scope. Should the potassco/anthem software project be a comprehensive toolkit for ASP verification, or a library supporting verification?
2. Project name. Based on the scope, is this project named Anthem, Anthem-Next, or ASPCtk?
3. Time to prepare a release to crates.io supporting (at minimum, tau* and a CLI).

Vladimir requested (Oct 19, 2023) the following modification to the parsing/formatting of integer/general variables:

"I like this. But it may be even better to adopt different conventions for variable names of two kinds: those that begin with I, J, K, L, M, N and those that begin with other letters. A variable of the first kind is integer unless it ends with $g; a variable of the second kind is general unless it ends with $i."

TRUE should be a logical primitive analogous to FALSE. Furthermore, empty conjunctions (empty disjunctions) should be simplified to TRUE (FALSE). Especially within the tau* translation, the treatment of a fact "p" is better understood as an empty conjunction of tau^B applied to body literals, which simplifies to "true -> p" rather than just translating it as "p"

Function constants that occur within a program (but are not specified as placeholders) need a unique name axiom added to Vampire problem files. For example, Patrick's code adds

tff(symbolic_constant_order, axiom, p__less__(a, b)).

to the problem file generated by the problem

( {p :- a != b}, {spec: p.} )

An unnamed inductive lemma is named "inductive-lemma" by default, but TPTP forbids the "-" symbol in formula names. We should probably change the parsing and formatting of the inductive lemma role to "inductive_lemma"

See strong equivalence examples from how that could look like.

Currently, predicate renaming always occurs (but it doesn't have to). We need to settle on cases when renaming isn't necessary with the goal of making lemma writing easier (e.g. don't have to name a predicate p as p_1 or p_2 when writing lemmas).