Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs.

Yukihide Takayama

Published in: J. Symb. Comput. (1991)

Keyphrases

natural deduction
theorem prover
cut elimination
inference rules
sequent calculus
theorem proving
intuitionistic logic
information extraction
linear logic
linear time temporal logic
training data
training set
fixpoint