Question answering with MANSEX
Overview
- Single answers extracted from proofs using
OAESys
- Multiple answers extracted through internal implementation of
MANSEX
- Answers provided as part of
result display
Augmented MANSEX
- Removes the conjecture augmentations
- Answer variables instantiated with answer
- Just the required axioms supplied
- Rerun ATP system to get proof for display