Một hệ thống chuẩn hóa của suy diễn tự nhiên cho logic tuyến tính trực giác

Kết quả chính của bài báo này là một hệ thống chuẩn hóa của suy diễn tự nhiên cho ngôn ngữ đầy đủ của logic tuyến tính trực giác. Không cần quy tắc làm yếu hoặc rút gọn rõ ràng cho các công thức - . Bằng cách sử dụng có hệ thống các quy tắc loại bỏ tổng quát, một sự tương ứng giữa các suy diễn chuẩn và các suy diễn không cắt trong phép tính chuỗi được thiết lập. Việc chuẩn hóa và thuộc tính tiểu công thức cho các suy diễn chuẩn xảy ra thông qua việc dịch sang phép tính chuỗi và loại bỏ cắt.