Conclusion

Encoding

• Basic encoding is quite straight forward
  • Used features of FOL ATP to encode tricky bits
• Definitional encoding scheme makes hard ATP
• Including everything (operators, operator definitions) may be overkill

Equivalences

• Some progress, but not much yet
• Either ...
  • I've made a mistake in the logic ... HELP!
  • The encoding is too cumbersome
  • These are hard problems for ATP

Future Work

• Resolve all the HELP! worries
• Do (== have a student do) a proper survey of techniques and other work
• First-order modal logic ... can it be done (this way)?
  • Variables at the modal level
  • Quantification at the modal level