sneeuwballen/zipperposition

Assertion failed

mcoulont opened this issue · 7 comments

mcoulont commented

Hi all

I'm not even sure I'm supposed to write here, you'll tell me if there's a problem.

When I run zipperposition on a file containing:

data nat := Zero | Succ nat.

def plus : nat -> nat -> nat where
  forall y. plus Zero y = y;
  forall x y. plus (Succ x) y = Succ (plus x y).

goal forall (x:nat) (y:nat). plus x y = plus y x.

I get "File "src/prover_calculi/induction.ml", line 238, characters 8-14: Assertion failed".

The problem seems to appear when the last of the 3 commands is run.

The error seems to occur deep in your code, I would hardly figure it out.

I've installed Zipperposition with opam and it's the 1.6 release.

Kind Regards
Marc

c-cube commented
mcoulont commented

Thanks for your answer.

Ok, so I should proceed manually to install Zipperposition (via git clone) ?

You've more or less let down the induction, but is there a maintained way to make some arithmetic ?

c-cube commented

The integer/rational arithmetic should still work. However, it's not maintained either and has never been super good (see results at CASC in 2014). Mixing arithmetic and superposition is still a research problem and other solvers tend to delegate most of the work to SMT solver (see: Beagle).

To install the master version: yes, a local git clone, and compile with make or use opam pin locally.

mcoulont commented

If you refer to (http://www.tptp.org/CASC/J7/WWWFiles/ResultsSummary.html) you did good for integers.

By "use opam pin locally", do you mean install opam and use "opam install" in the cloned folder ?

c-cube commented
mcoulont commented

It ended up working, thanks.

Must I close the ticket ?

By the way, is there a way to import files ? But perhaps this kind of stuff is more suited to SMT ?

With my PC (i7, 16 Go, Ubuntu 20) the associativity of multiplication was proved in 159s and its commutativity wasn't proved at all (the engine keeps computing, with no result). Is it normal ?

c-cube commented

There isn't a way to import files in .zf files (nor in smt files). Only TPTP has such a feature, and it's not necessarily a good idea (read about the $TPTP env variable…).

I'll close the issue.

With my PC (i7, 16 Go, Ubuntu 20) the associativity of multiplication was proved in 159s and its commutativity wasn't proved at all (the engine keeps computing, with no result). Is it normal ?

Possibly? Is the associativity of multiplication done from scratch? All files in examples are not meant to pass successfully, some are just too hard. Induction is a hard problem 🙂