Equational reasoning in Isabelle (Q1825045)

Isabelle is an interactive theorem prover developed at the University of Cambridge. It differs from most other theorem provers in the fact that it can be parameterized by the object-logic to be used. This feature made it possible to carry out a case study in an equational logic - a fragment of the first-order predicate calculus. A number of used specific tactics, embodying theorem proving techniques in that logic, are described. Though an efficiency of the process is not discussed it proves feasibility of the selected approach.