zachjhansen / zanthem-next Goto Github PK

Currently the Problem::from_components and Problem::from_derivation_components will overwrite files in out-dir since all problems in the sequence have the same name - need to add an iterator e.g. problem_1, problem_2, etc.

The issue you encountered was because currently every placeholder needs its own line, e.g.

Input: a$i.
Input: b$i.

Collapsing these statements onto one line is a work-in-progress improvement.

If the user does not name an inductive lemma F, then the TPTP format will produce

tff( _base_case, conjecture, F).

This is an error - Vampire does not accept formula names beginning with an underscore. So if the formula is unnamed, then the inductive lemma should just be named "base_case" rather than "_base_case"

Hi Zach,

By making function constants explicitly sorted, parsing specs or lemmas can be accomplished independent of context (the provided user guide).

Let’s try to find a way to achieve your goal—parsing formulas independent of context—without the unfortunate side effect of introducing two different names for the same placeholder.

What if we treat every placeholder as a constant of the sort “general”? That will make p(n+1) syntactically incorrect even when n is a placeholder, but this is okay; we can write

exists N ( N = n and p(N+1) ).

This is the same trick that we use with general variables: since p(X+1) is not allowed, we write

exists N ( N = X and p(N+1) ).

The statement

input: n$i.

(or n -> integer, as in the old antem—whichever you like better) will have the same meaning as

input n.
assumption: exists N (N = n).

As I understand, you can help vampire to speed up search by using the sort integer when you represent n in the TPTP language. But this is an implementation detail, not related to the meaning of the input statement.

What do you think?

Best,
Vladimir

Allow:
./anthem verify .{ext1, ext2, ext3}

as an abbreviation for ./anthem verify .ext1 .ext2 .ext3

The "parsing" example fails due to conflict between symbolic constant "t" and predicate "t/0".

Definitions should always be universal - or logic should be added to address the following scenario:

definition(forward): p <-> q.
definition(backward): g <-> p.

this is an invalid sequence of definitions since g depends on p, yet the definition of p is not defined for the backward direction.

forall N$ (N$ >= 1 -> (not exists M$ sqrtb(M$) -> N$*N$ <= b$i))

This formula is not long, but to us humans it looks a little strange. It will be easier to understand what we are actually proving by induction is we rewrite that formula as

not exists M$ sqrtb(M$) -> forall N$ (N$ >= 1 -> N$*N$ <= b$i).

This observation suggests that it would be useful to allow “conditional” inductive lemmas:

C -> forall N$ ( … -> … ),

where C is a formula without free variables. It should be processed exactly as

forall N$ ( C and … -> … ).

allow the “n$” abbreviation for “n$i”.