ในตรรกศาสตร์ทางคณิตศาสตร์ระบบการพิสูจน์หรือแคลคูลัสการพิสูจน์ถูกสร้างขึ้นเพื่อพิสูจน์ข้อความต่างๆ

ระบบการพิสูจน์ประกอบด้วยส่วนประกอบดังต่อไปนี้: ^{[ 1 ] [ 2 ]}

• ภาษาเชิงรูปธรรม : เซตLของสูตรที่ระบบยอมรับ เช่นตรรกศาสตร์เชิงประพจน์หรือตรรกศาสตร์อันดับหนึ่ง
• กฎการอนุมาน : รายชื่อกฎที่สามารถนำมาใช้พิสูจน์ทฤษฎีบทจากสัจพจน์และทฤษฎีบทได้
• สัจพจน์ : สูตรในภาษา Lที่ถือว่าถูกต้องทฤษฎีบท ทั้งหมด ได้มาจากการสัจพจน์

การพิสูจน์อย่างเป็นทางการของสูตรที่มีรูปแบบดีในระบบการพิสูจน์คือชุดของสัจพจน์และกฎการอนุมานของระบบการพิสูจน์ที่อนุมานว่าสูตรที่มีรูปแบบดีเป็นทฤษฎีบทของระบบการพิสูจน์^{[ 2 ]}

โดยปกติแล้ว แคลคูลัสการพิสูจน์ที่กำหนดไว้จะครอบคลุมมากกว่าหนึ่งระบบเชิงรูปธรรมเฉพาะ เนื่องจากแคลคูลัสการพิสูจน์จำนวนมากมีตัวกำหนดไม่ครบถ้วนและสามารถใช้กับตรรกะที่แตกต่างกันอย่างสิ้นเชิงได้ ตัวอย่างเช่น กรณีตัวอย่างคือแคลคูลัสลำดับซึ่งสามารถใช้เพื่อแสดงความสัมพันธ์ของผลลัพธ์ของทั้งตรรกะเชิงสัญชาตญาณและตรรกะเชิงความเกี่ยวข้องดังนั้น โดยคร่าวๆ แล้ว แคลคูลัสการพิสูจน์คือแม่แบบหรือรูปแบบการออกแบบซึ่งมีลักษณะเฉพาะด้วยรูปแบบของการอนุมานเชิงรูปธรรมบางอย่าง ที่อาจถูกปรับแต่งเพื่อสร้างระบบเชิงรูปธรรมเฉพาะ โดยการระบุถึงกฎการอนุมานที่แท้จริงสำหรับระบบดังกล่าว ไม่มีฉันทามติในหมู่นักตรรกศาสตร์เกี่ยวกับวิธีการกำหนดคำนี้ให้ดีที่สุด

สูตรคำนวณพิสูจน์ที่เป็นที่รู้จักกันอย่างแพร่หลายมากที่สุด คือสูตรคำนวณแบบคลาสสิกที่ยังคงใช้กันอย่างแพร่หลายในปัจจุบัน:

• คลาสของระบบฮิลเบิร์ต [ ^{2 ]}ซึ่งตัวอย่างที่มีชื่อเสียงที่สุดคือ^ระบบตรรกะลำดับที่หนึ่งของฮิลเบิร์ต-แอคเคอร์แมนใน ปี 1928
• แคลคูลัสการอนุมานตามธรรมชาติ ของ เกอร์ฮาร์ด เกนท์เซนซึ่งเป็นรูปแบบแรกของทฤษฎีการพิสูจน์เชิงโครงสร้างและเป็นรากฐานของการจับคู่สูตรเป็นประเภทที่เชื่อมโยงตรรกศาสตร์กับการเขียนโปรแกรมเชิงฟังก์ชัน
• แคลคูลัสลำดับของเกนท์เซนซึ่งเป็นรูปแบบทางทฤษฎีการพิสูจน์เชิงโครงสร้างที่ได้รับการศึกษามากที่สุด

วิธีคำนวณพิสูจน์อื่นๆ อีกมากมายนั้น อาจเป็นวิธีการที่สำคัญ แต่ปัจจุบันไม่ได้ถูกนำมาใช้กันอย่างแพร่หลาย

• ตรรกบท เชิงตรรกะของ อริสโตเติลซึ่งนำเสนอไว้ในหนังสือออร์กาโนนสามารถนำหลักการทางตรรกบทมาใช้ในรูปแบบที่เป็นทางการได้อย่างง่ายดาย ปัจจุบันก็ยังมีความสนใจในตรรก บทเชิงตรรกะอยู่ บ้างโดยดำเนินการภายใต้กรอบของ ตรรก บทเชิงคำศัพท์
• สัญกรณ์สองมิติของGottlob Frege ใน Begriffsschrift (1879) มักถูกมองว่าเป็นการนำแนวคิดสมัยใหม่ของตัวบ่งปริมาณมาสู่ตรรกศาสตร์
• กราฟแสดงการดำรงอยู่ของซี.เอส. เพียร์ซอาจกลายเป็นผลงานชิ้นสำคัญได้ หากประวัติศาสตร์เป็นไปในทิศทางที่แตกต่างออกไป

งานวิจัยสมัยใหม่ในสาขาตรรกศาสตร์เต็มไปด้วยวิธีการคำนวณพิสูจน์ที่แข่งขันกัน:

• มีการเสนอระบบหลายระบบที่ใช้ไวยากรณ์เชิงกราฟิกแทนไวยากรณ์ข้อความแบบเดิม โดยระบบพิสูจน์โครงข่ายและแคลคูลัสเชิงวงจรเป็นหนึ่งในระบบเหล่านั้น
• เมื่อไม่นานมานี้ นักตรรกศาสตร์หลายคนที่สนใจทฤษฎีการพิสูจน์เชิงโครงสร้างได้เสนอแคลคูลัสที่มีการอนุมานเชิงลึกตัวอย่างเช่นตรรกศาสตร์แสดงผล (display logic) , ไฮเปอร์ซีเควนต์ (hypersequents) , แคลคูลัสของโครงสร้าง (calculus of structures)และ การบ่งชี้ แบบกลุ่ม (bunched implication )

• วิธีการของตารางวิเคราะห์
• ขั้นตอนการพิสูจน์
• ระบบการพิสูจน์เชิงประพจน์
• ความละเอียด (ตรรกะ)