src/FOL/intprover.ML
changeset 1005 65188e520024
parent 702 98fc1a8e832a
child 1459 d12da312eff4
equal deleted inserted replaced
1004:70676af0ac97 1005:65188e520024
     9 
     9 
    10 Completeness (for propositional logic) is proved in 
    10 Completeness (for propositional logic) is proved in 
    11 
    11 
    12 Roy Dyckhoff.
    12 Roy Dyckhoff.
    13 Contraction-Free Sequent Calculi for Intuitionistic Logic.
    13 Contraction-Free Sequent Calculi for Intuitionistic Logic.
    14 J. Symbolic Logic (in press)
    14 J. Symbolic Logic  57(3), 1992, pages 795-807.
       
    15 
       
    16 The approach was developed independently by Roy Dyckhoff and L C Paulson.
    15 *)
    17 *)
    16 
    18 
    17 signature INT_PROVER = 
    19 signature INT_PROVER = 
    18   sig
    20   sig
    19   val best_tac: int -> tactic
    21   val best_tac: int -> tactic