SEKI Report
Refine
Year of publication
- 1998 (4) (remove)
Document Type
- Preprint (4)
Language
- English (4)
Has Fulltext
- yes (4)
Keywords
- HOT (1)
- Simultaneous quantifier elimination (1)
- automated proof planner (1)
- higher order tableau (1)
- natural language semantics (1)
- proof presentation (1)
- sequent calculus (1)
- skolemization (1)
- theorem prover (1)
Faculty / Organisational entity
98,4
This paper describes a tableau-based higher-order theorem prover HOT and an application to natural language semantics. In this application, HOT is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections.
98,8
The paper addresses two problems of comprehensible proof presentation, the hierarchically structured presentation at the level of proof methods and different presentation styles of construction proofs. It provides solutions for these problems that can make use of proof plans generated by an automated proof planner.
98,5
Simultaneous quantifier elimination in sequent calculus is an improvement over the well-known skolemization. It allows a lazy handling of instantiations as well as of the order of certain reductions. We prove the soundness of a sequent calculus which incorporates a rule for simultaneous quantifier elimination. The proof is performed by semantical arguments and provides some insights into the dependencies between various formulas in a sequent.