Suy diễn & quy tắc suy luận
Suy diễn tự nhiên: viết chứng minh logic từng dòng có lý do rõ ràng
Suy diễn tự nhiên viết chứng minh thành từng dòng, mỗi dòng là tiền đề, giả định tạm hoặc kết quả một quy tắc nhập, khử. Gentzen và Jaśkowski đề xuất năm 1934.