推論形式
演繹法
α₁ ∀x.A(x)→B(x)
α₂ A[x,e]
β B[x,e]
帰納法
α₁ A[x,e]
α₂ B[x,e]
β ∀x.A(x)→B(x)
遡測法
α₁ ∀x.A(x)→B(x)
α₂ B[x,e]
β A[x,e]
類推
α₁ A[x,e]
α₂ B[x,e]
α₃ A[x,e']
β B[x,e']
演繹法
α₁ ∀x.A(x)→B(x)
α₂ A[x,e]
β B[x,e]
帰納法
α₁ A[x,e]
α₂ B[x,e]
β ∀x.A(x)→B(x)
遡測法
α₁ ∀x.A(x)→B(x)
α₂ B[x,e]
β A[x,e]
類推
α₁ A[x,e]
α₂ B[x,e]
α₃ A[x,e']
β B[x,e']