edggy / pyLemma

A formal proof creating tool in Python
MIT License
1 stars 2 forks source link

Generalization (?) #1

Open ghost opened 8 years ago

ghost commented 8 years ago

The use of generalized inference rules would be very helpful.

Example 1:

and(A, B, C, D, E, F)
#---------------------
and(B, D, E)

Example 2:

or(A, B, C)
|-(A, S)
|-(B, S)
|-(C, S)
#-----------
S
edggy commented 7 years ago

Possible syntax can be

and(...A...)
#------------
A
or(...A...)
...
|-(A, S)
...
#-----------
S

Where "...A..." would stand for an arbitrary argument and the "..." before and after the "|-(A, S)" denote we need this for each possible "A"