options

(here, you can control some options of Alt-Ergo)

Max Steps

» Number of calls to the decision procedures by the SAT solver

Max Triggers

» Number of patterns per axiom. These patterns are used when instantiating universally quantified formulas

Max Splits

» Maximum size of opened case-splits

No E-matching

» Use simple matching when instantiating (deactivate 'modulo ground equalities')

Used Context

» Highlight the quantified axioms and predicates that are used for the proof. The result is shown in 'Statistics' section (beta)

Debug

» Print some information in 'Debug' section to debug data exchange with Alt-Ergo

Input Language

» Select the input language of the given formula

debug

(some basic debug information are printed here)

examples

(click on an example to load it in the right panel)

» Linear Arithmetic

goal g_1 :
  forall x,y,z,t:int.
    0 <= y + z <= 1  -> 
    x + t + y + z = 1 -> 
    y + z <> 0 -> 
    x + t = 0

» Uninterpreted functions and Arithmetic

logic h,g,f: int,int -> int
logic a, b:int

goal g_2 :
  h(g(a,a),g(b,b)) = g(b,b) ->
  a = b ->
  g(f(h(g(a,a),g(b,b)),b) - f(g(b,b),a),
    f(h(g(a,a),g(b,b)),a) - f(g(b,b),b)) = g(0,0)

» Quantifiers

type 'a pointer
type 'a pset

logic P : int -> prop
logic Q : int , int -> prop

axiom a:
  (forall x:int.
     (P(x) <-> 
	(exists i:int. 
	   exists r: int. Q(r,i))))

goal g_3 : 
  Q(1,2) -> 
  P(4)

» Polymorphism

type 'a set

logic empty : 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop

axiom mem_empty:
  forall x : 'a.
  not mem(x, empty : 'a set)

axiom mem_add:
  forall x, y : 'a. forall s : 'a set.
  mem(x, add(y, s)) <->
  (x = y or mem(x, s))

logic is1, is2 : int set
logic iss : int set set

goal g_4:
  is1 = is2 -> 
  (not mem(1, add(2+3, empty : int set))) and
  mem (is1, add (is2, iss))

» Arrays

goal g_5 :
  forall i,j,k:int.
  forall v,w : 'a.
  forall b : 'a farray.
  b = b[j<-b[i],k<-w] ->
  i = 1 ->
  j = 2 -> 
  k = 1 -> 
  b[i] = b[j]

» Enumerations and Arrays

type t = A | B | C | D
type t2 = E | F | G | H

goal g_6 :
     forall a : (t,t2) farray.
     a[B <- E][A] <> E ->
     a[C <- F][A] <> F ->
     a[D <- G][A] <> G ->
     a[A] = H

» Non-linear Arithmetic

goal g_7 :
  forall x,y,z:int.
  x > 3  ->
  y > 0 ->
  z > 0  ->
  y > z  ->
  z = ((x / y) + y) / 2 -> 
  z > 1 and y > 2

goal g_8 :
  forall x,y:int.
  x > 3 ->
  y = (x + 1) / 2 ->
  x < (y + 1) * (y + 1)

goal g_9 :
  forall a,b:int. 
  a > 0  -> 
  a % 2 = 1 -> 
  b + (a / 2) * (2 * b) = a * b

Options

Statistics

Debug

Examples

About

Load a Local File

This is "Try Alt-Ergo" Version "Unknown"
							
							The output of Alt-Ergo will appear here. Click on "Debug" or "Statistics" sections to see more information.