Conclusion

This Work

• Looked at what we Need and Have from interpretations
• Described a flexible format for D&M interpretations
• Presented some tools for playing with interpretations
• Is hoping for community approval

Forthcoming Attractions

• Fix the format for saturations
• Investigate how to verify saturations
• Fix the format for Herbrand interpretations as formulae
• Think about how SMT represents and verifies its models