Linking Other Theorem Provers to HOL Using PM: Proof Manager.

Myla Archer George Fink Lie Yang

Published in: TPHOLs (1992)

Keyphrases

theorem prover
theorem proving
automated theorem proving
natural deduction
higher order logic
automated reasoning

inference rules
formal proof
first order logic
proof search
automated deduction

term rewriting
formal semantics
computer algebra
timed automata
proof planning

management system
distributed systems
higher order
sequent calculus
expert systems