Calling External Provers
Init
Otter Example (First Order Logic with Equality) - "Equality is Transitive"
show
Converted by
Mathematica
June 17, 2002
![[Graphics:../Images/index_gr_46.gif]](../Images/index_gr_46.gif)
![[Graphics:../Images/index_gr_47.gif]](../Images/index_gr_47.gif)
![[Graphics:../Images/index_gr_48.gif]](../Images/index_gr_48.gif)
![[Graphics:../Images/index_gr_49.gif]](../Images/index_gr_49.gif){kind=small}