Automating Type Soundness Proofs via Decision Procedures and Guided Reductions.

Don Syme Andrew D. Gordon

Published in: LPAR (2002)

Keyphrases

decision procedures
theorem proving
modal logic
automated reasoning
reasoning problems
quantified boolean formulas
artificial intelligence
conjunctive queries
satisfiability problem
special case
knowledge representation