The Isabelle proof assistant comes equipped with a very powerful tactic for term simplification. While tremendously useful, the results of simplifying a term do not always match the user’s expectation: sometimes, the resulting term is not in the form the user expected, or the simplifier fails to apply a rule. We describe a new, interactive tracing facility which offers insight into the hierarchical structure of the simplification with user-defined filtering, memoization and search. The new simplifier trace is integrated into the Isabelle jEdit Prover IDE.
Part 1 Logic programs: basic constructs database programming recursive programming the computation model of logic programs theory of logic programs. Part 2 The Prolog language: pure Prolog programming in pure Prolog arithmetic structure inspection meta-logical predicates cuts and negation extra-logical predicates program development. Part 3 Advanced Prolog programming techniques: nondeterministic programming incomplete data structures second-order programming interpreters program transformation logic grammars search techniques. Part 4 Applications: game-playing programs a credit evaluation expert system an equation solver a compiler. Appendix: operators. PROLOG, logic programming based languages, became very popular in the eighties, taking a circuitous route to the United States; from Europe to Japan to mainstream American computer science.