Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment.

Ramayya Kumar Klaus Schneider Thomas Kropf

Published in: Formal Methods Syst. Des. (1993)

Keyphrases

theorem proving
higher order
theorem prover
decision procedures
real time
first order logic

automated deduction
automated reasoning
inference rules
automatic programming
parallel search
term rewriting

consequence finding
proof procedure
geometry theorem proving
proof planning
logical inference

predicate calculus
proof search
automated theorem proving
pairwise
timed automata