What do we Have?
Finite Domains + Mappings
☞
- Enumeration of domains' elements
- Mappings for all symbols - ground or quantified
- Examples: Mace4, Paradox, Vampire
- Verifiable✓
Comprehensible✓
^C-tolerable✓
Infinite Domains + Mappings
☞
- Specification of domains' elements - terms, e.g., Peano, or defined, e.g., $int
- Mappings for all symbols, e.g., universal quantification
- Examples: cvc5, FEST Z3
- Verifiable✓
Comprehensible✓
^C-tolerable✗
Saturations as Herbrand Interpretations
☞
- Set of clauses
- Has the same models as the input - can derive input
- Examples: SPASS, E, Vampire
- Verifiable✓
Comprehensible✗
^C-tolerable✗
Formulae as Herbrand Interpretations
☞
- Predicate definitions over the term algebra (old DIGs)
- Define truth for Herbrand Base
- Examples: iProver
- Compact, quite some work to produce them
- Verifiable✓
Comprehensible?
^C-tolerable?
Kripke Interpretations
☞
- Worlds - finite or infinite
- Interpretation in a world - see above
- Accessibility relation - ground or quantified
- Examples: KSP, MoMo
- Verifiable?
Comprehensible?
^C-tolerable?