Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

failure in ViperTest #596

Closed
shetzl opened this issue Jan 4, 2017 · 4 comments
Closed

failure in ViperTest #596

shetzl opened this issue Jan 4, 2017 · 4 comments

Comments

@shetzl
Copy link
Member

shetzl commented Jan 4, 2017

I currently get the following test failure:

[info] ViperTest
[info] 
[info] known to be working problems
[info]   + appnil
[info]   + comm
[info]   + comm1
[info]   + commsx
[info]   + comms0
[info]   + general
[info]   + generaldiffconcl
[info]   + linear
[info]   o linear2par
[info] needs careful choice of instance for canonical substitution
[info]   + square
[info]   + minus
[error]   ! plus0
[error]    scala.MatchError: None (of class scala.None$) (Viper.scala:189)
[error] at.logic.gapt.provers.viper.Viper.solveSPWI(Viper.scala:189)
[error] at.logic.gapt.provers.viper.Viper.solve(Viper.scala:122)
[error] at.logic.gapt.provers.viper.ViperTest.$anonfun$new$3(ViperTest.scala:37)
[info] 
[info]   + prod_prop_31
[info]   + prod_prop_31_monomorphic
[info] 
[info] 
[info] Total for specification ViperTest
[info] Finished in 36 seconds, 645 ms
[info] 14 examples, 0 failure, 1 error, 1 skipped
[info] 
[error] Error: Total 14, Failed 0, Errors 1, Passed 12, Skipped 1
[error] Error during tests:
[error]         at.logic.gapt.provers.viper.ViperTest
[error] (tests/test:testQuick) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 51 s, completed 04.01.2017 12:06:30

Any ideas?
@gebner
Copy link
Member

gebner commented Jan 4, 2017

Can you post the output of bestAvailableMaxSatSolver.actualSolver (on the CLI), and the output of viper examples/induction/plus0.smt?

@shetzl
Copy link
Member Author

shetzl commented Jan 4, 2017 

gapt> bestAvailableMaxSatSolver.actualSolver
res0: at.logic.gapt.provers.maxsat.MaxSATSolver = at.logic.gapt.provers.maxsat.QMaxSAT$@5c740c5a

stefan@clogic83:~/Uni/Software/gapt-devel/rep/gapt$ ./viper.sh examples/induction/plus0.smt2 
∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x
Proving instance List(s(o))
Instance proof for List(s(o)):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-)
:-
(plus(o, s(o)) = s(o))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
's0:plus(o,x)=x':_Inst                                                                                                                                                                                                                       
Proving instance List(o)                                                                                                                                                                                                                     
Instance proof for List(o):                                                                                                                                                                                                                  
∀x plus(x, o) = x +^{o} (plus(o, o) = o)- :- (plus(o, o) = o)+                                                                                                                                                                               
Language:                                                                                                                                                                                                                                    
'a1:plus(x,o)=x'(o:nat): _Inst                                                                                                                                                                                                               
's0:plus(o,x)=x':_Inst                                                                                                                                                                                                                       
Found schematic proof with induction:                                                                                                                                                                                                        
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,                                                                                                                                                                                    
∀x (plus(x:nat, o:nat): nat) = x,                                                                                                                                                                                                            
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),                                                                                                                                                                                                      
∀y0 ¬o = s(y0)                                                                                                                                                                                                                               
⊢                                                                                                                                                                                                                                            
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>nat>o                                                                                                                                                                                    
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat                                                                                                                                                                                 
                                                                                                                                                                                                                                             
A(x0) → plus(o, o) = o                                                                                                                                                                                                                       
A(x0) → plus(o, s(o)) = s(plus(o, o))                                                                                                                                                                                                        
B(x0, x1, x2) → plus(o, o) = o                                                                                                                                                                                                               
B(x0, x1, x2) → plus(o, s(o)) = s(plus(o, o))                                                                                                                                                                                                
,BaseTypes: nat, o, sk                                                                                                                                                                                                                       
                                                                                                                                                                                                                                             
Constants:                                                                                                                                                                                                                                   
  s: nat>nat                                                                                                                                                                                                                                 
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(o)))
Proving instance List(s(s(o)))
Instance proof for List(s(s(o))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-)
:-
(plus(o, s(s(o))) = s(s(o)))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → plus(o, s(o)) = s(plus(o, o))
A(x0) → plus(o, s(s(o))) = s(plus(o, s(o)))
B(x0, x1, x2) → plus(o, o) = o
B(x0, x1, x2) → plus(o, s(o)) = s(plus(o, o))
B(x0, x1, x2) → plus(o, s(s(o))) = s(plus(o, s(o)))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(s(o))))
Proving instance List(s(s(s(o))))
Instance proof for List(s(s(s(o)))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-
      +^{s(s(o))} (plus(o, s(s(s(o)))) = s(plus(o, s(s(o)))))-)
:-
(plus(o, s(s(s(o)))) = s(s(s(o))))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(o): nat)): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → plus(o, s(o)) = s(plus(o, o))
A(x0) → plus(o, s(s(o))) = s(plus(o, s(o)))
A(x0) → plus(o, s(s(s(o)))) = s(plus(o, s(s(o))))
B(x0, x1, x2) → plus(o, o) = o
B(x0, x1, x2) → plus(o, s(o)) = s(plus(o, o))
B(x0, x1, x2) → plus(o, s(s(o))) = s(plus(o, s(o)))
B(x0, x1, x2) → plus(o, s(s(s(o)))) = s(plus(o, s(s(o))))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(s(s(o)))))
Proving instance List(s(s(s(s(o)))))
Instance proof for List(s(s(s(s(o))))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-
      +^{s(s(o))} (plus(o, s(s(s(o)))) = s(plus(o, s(s(o)))))-
      +^{s(s(s(o)))} (plus(o, s(s(s(s(o))))) = s(plus(o, s(s(s(o))))))-)
:-
(plus(o, s(s(s(s(o))))) = s(s(s(s(o)))))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(o): nat)): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(s(o): nat))): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → B(x0, x0, o)
B(x0, o, x2) → plus(o, o) = o
B(x0, o, x2) → plus(o, s(x2)) = s(plus(o, x2))
B(x0, s(x1_0), x2) → plus(o, o) = o
B(x0, s(x1_0), x2) → plus(o, s(x2)) = s(plus(o, x2))
B(x0, s(x1_0), x2) → B(x0, x1_0, s(x2))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(o))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(o)))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(o))))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(s(o)))))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(s(s(o))))))))))))))): true
Solution condition:
∃X_B (∀x_2 ∀x_0 (plus(o, o) = o ∧ plus(o, s(x_2)) = s(plus(o, x_2)) ⊃
        X_B(x_0:nat, o, x_2)) ∧
    ∀x_0 ∀x_2 ∀x_3 (plus(o, o) = o ∧
          X_B(x_0, x_2, s(x_3)) ∧
          plus(o, s(x_3)) = s(plus(o, x_3)) ⊃
        X_B(x_0, s(x_2), x_3)) ∧
    ∀x (plus(o, o) = o ∧ X_B(x, x, o) ⊃ plus(o, x) = x))

Canonical solution at X_B(y_0:nat, s(s(o)), w_0:nat): o:
 :- plus(o, s(w_0)) = s(plus(o, w_0))
 :- plus(o, s(s(w_0))) = s(plus(o, s(w_0)))
 :- plus(o, s(s(s(w_0)))) = s(plus(o, s(s(w_0))))
 :- plus(o, o) = o
^[[6~Exception in thread "main" scala.MatchError: None (of class scala.None$)
        at at.logic.gapt.provers.viper.Viper.solveSPWI(Viper.scala:189)
        at at.logic.gapt.provers.viper.Viper.solve(Viper.scala:122)
        at at.logic.gapt.provers.viper.Viper$.main(Viper.scala:276)
        at at.logic.gapt.provers.viper.Viper.main(Viper.scala)

@gebner
Copy link
Member

gebner commented Jan 4, 2017

Can you try again, please?

@shetzl
Copy link
Member Author

shetzl commented Jan 4, 2017

Now it works, thanks. sbt test completes successfully and viper.sh says:

stefan@clogic83:~/Uni/Software/gapt-devel/rep/gapt$ ./viper.sh examples/induction/plus0.smt2 
∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x
Proving instance List(o)
Instance proof for List(o):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)- :- (plus(o, o) = o)+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
's0:plus(o,x)=x':_Inst
Proving instance List(s(o))
Instance proof for List(s(o)):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-)
:-
(plus(o, s(o)) = s(o))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → plus(o, s(o)) = s(plus(o, o))
B(x0, x1) → plus(o, o) = o
B(x0, x1) → plus(o, s(o)) = s(plus(o, o))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(o)))
Proving instance List(s(s(o)))
Instance proof for List(s(s(o))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-)
:-
(plus(o, s(s(o))) = s(s(o)))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → plus(o, s(o)) = s(plus(o, o))
A(x0) → plus(o, s(s(o))) = s(plus(o, s(o)))
B(x0, x1) → plus(o, o) = o
B(x0, x1) → plus(o, s(o)) = s(plus(o, o))
B(x0, x1) → plus(o, s(s(o))) = s(plus(o, s(o)))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(s(o))))
Proving instance List(s(s(s(o))))
Instance proof for List(s(s(s(o)))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-
      +^{s(s(o))} (plus(o, s(s(s(o)))) = s(plus(o, s(s(o)))))-)
:-
(plus(o, s(s(s(o)))) = s(s(s(o))))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(o): nat)): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → plus(o, s(o)) = s(plus(o, o))
A(x0) → plus(o, s(s(o))) = s(plus(o, s(o)))
A(x0) → plus(o, s(s(s(o)))) = s(plus(o, s(s(o))))
B(x0, x1) → plus(o, o) = o
B(x0, x1) → plus(o, s(o)) = s(plus(o, o))
B(x0, x1) → plus(o, s(s(o))) = s(plus(o, s(o)))
B(x0, x1) → plus(o, s(s(s(o)))) = s(plus(o, s(s(o))))
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): false
Minimal counterexample: List(s(s(s(s(o)))))
Proving instance List(s(s(s(s(o)))))
Instance proof for List(s(s(s(s(o))))):
∀x plus(x, o) = x +^{o} (plus(o, o) = o)-,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1))
  +^{o}
    (∀y1 plus(o, s(y1)) = s(plus(o, y1))
      +^{o} (plus(o, s(o)) = s(plus(o, o)))-
      +^{s(o)} (plus(o, s(s(o))) = s(plus(o, s(o))))-
      +^{s(s(o))} (plus(o, s(s(s(o)))) = s(plus(o, s(s(o)))))-
      +^{s(s(s(o)))} (plus(o, s(s(s(s(o))))) = s(plus(o, s(s(s(o))))))-)
:-
(plus(o, s(s(s(s(o))))) = s(s(s(s(o)))))+
Language:
'a1:plus(x,o)=x'(o:nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, o): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(o): nat): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(o): nat)): _Inst
'a2:plus(x,s(y1))=s(plus(x,y1))'(o:nat, s(s(s(o): nat))): _Inst
's0:plus(o,x)=x':_Inst
Found schematic proof with induction:
ProofByRecursionScheme(∀x0 (p(s(x0:nat): nat): nat) = x0,
∀x (plus(x:nat, o:nat): nat) = x,
∀x ∀y1 plus(x, s(y1)) = s(plus(x, y1)),
∀y0 ¬o = s(y0)
⊢
∀x plus(o, x) = x,Non-terminals: A:nat>o, B:nat>nat>o
Terminals: '=':nat>nat>o, o:nat, plus:nat>nat>nat, s:nat>nat

A(x0) → plus(o, o) = o
A(x0) → B(x0, x0)
B(x0, o) → plus(o, o) = o
B(x0, s(x1_0)) → plus(o, o) = o
B(x0, s(x1_0)) → plus(o, s(x1_0)) = s(plus(o, x1_0))
B(x0, s(x1_0)) → B(x0, x1_0)
,BaseTypes: nat, o, sk

Constants:
  s: nat>nat
  plus: nat>nat>nat
  =: ?x>?x>o
  ∀: (?x>o)>o
  ⊃: o>o>o
  ∧: o>o>o
  ¬: o>o
  ⊤: o
  p: nat>nat
  ∃: (?x>o)>o
  ∨: o>o>o
  ⊥: o
  o: nat

StructurallyInductiveTypes:
  nat: o:nat, s:nat>nat
  o: ⊤, ⊥

Updates:
  InductiveType(o,Vector(⊤, ⊥))
  ConstDecl('¬')
  ConstDecl('∧')
  ConstDecl('∨')
  ConstDecl('⊃')
  ConstDecl('∀')
  ConstDecl('∃')
  ConstDecl('=')
  Sort(sk)
  InductiveType(nat,Vector(o:nat, s:nat>nat))
  ConstDecl(p:nat>nat)
  ConstDecl(plus:nat>nat>nat)
)

Checking validity for instance List(o): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(o)))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(o))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(o)))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(o))))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(s(o)))))))))))))): true
Checking validity for instance List(s(s(s(s(s(s(s(s(s(s(s(s(s(s(o))))))))))))))): true
Solution condition:
∃X_B (∀x_0 (plus(o, o) = o ⊃ X_B(x_0:nat, o)) ∧
    ∀x_2 ∀x_0 (plus(o, o) = o ∧
          plus(o, s(x_2)) = s(plus(o, x_2)) ∧
          X_B(x_0, x_2) ⊃
        X_B(x_0, s(x_2))) ∧
    ∀x (plus(o, o) = o ∧ X_B(x, x) ⊃ plus(o, x) = x))

Canonical solution at X_B(y_0:nat, s(o)): o:
 :- plus(o, o) = o
 :- plus(o, s(o)) = s(plus(o, o))
Found solution: λ(x0:nat) λx1 plus(o, x1) = x1

Found proof with 17 inferences

@shetzl shetzl closed this as completed Jan 4, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gebner @shetzl