Type detection with theorem prover

[Bart Bogaerts]

If some theory entails

!x y z: P(x,y,z) => T(x), and $T$ is known, then we can replace the signature of P by

P(X\capT,Y,Z)

(might be useful for the ASP competition)