ระบบตรวจสอบต้นแบบ ( PVS ) เป็นภาษากำหนดคุณสมบัติที่ผสานรวมกับเครื่องมือสนับสนุนและตัวพิสูจน์ทฤษฎีบทอัตโนมัติซึ่งพัฒนาขึ้นที่ห้องปฏิบัติการวิทยาศาสตร์คอมพิวเตอร์ของSRI Internationalในเมืองเมนโลพาร์ค รัฐแคลิฟอร์เนีย

PVS มีพื้นฐานมาจากแกนหลักที่ประกอบด้วยส่วนขยายของทฤษฎีประเภทของChurch ที่มี ประเภทแบบพึ่งพาและโดยพื้นฐานแล้วเป็นตรรกะลำดับสูงแบบคลาสสิกที่มีประเภท ประเภทพื้นฐานประกอบด้วยประเภทที่ไม่ถูกตีความซึ่งผู้ใช้สามารถกำหนดได้ และประเภทในตัว เช่น บูลีน จำนวนเต็ม จำนวนจริง และจำนวนเชิงอันดับ ตัวสร้างประเภทประกอบด้วยฟังก์ชัน เซต ทูเปิล เรคอร์ด การแจงนับ และประเภทข้อมูลนามธรรม ประเภทย่อยของ述语และประเภทแบบพึ่งพาสามารถใช้เพื่อกำหนดข้อจำกัดได้ ประเภทที่มีข้อจำกัดเหล่านี้อาจก่อให้เกิดภาระผูกพันในการพิสูจน์ (เรียกว่าเงื่อนไขความถูกต้องของประเภทหรือ TCC) ในระหว่างการตรวจสอบประเภท ข้อกำหนดของ PVS ถูกจัดระเบียบเป็นทฤษฎีแบบพารามิเตอร์

ระบบนี้ถูกพัฒนาขึ้นโดยใช้ภาษา Common Lispและเผยแพร่ภายใต้สัญญาอนุญาตทั่วไปของ GNU (GPL)

• วิธีการที่เป็นทางการ
• รายชื่อผู้ช่วยพิสูจน์อักษร
• โรเซตตา-ลัง

• เว็บไซต์ PVSที่ห้องปฏิบัติการวิทยาศาสตร์คอมพิวเตอร์ของSRI International
• บทสรุปของ PVSโดยJohn Rushbyใน ฐานข้อมูล Mechanized ReasoningของMichael KohlhaseและCarolyn Talcott
• PVSgymคือสภาพแวดล้อมการเรียนรู้แบบเสริมแรงสำหรับ PVS

บทความเกี่ยวกับภาษาโปรแกรมนี้ ยังเป็น เพียงบทความย่อคุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี

บทความเกี่ยวกับตรรกศาสตร์นี้ ยัง ไม่สมบูรณ์คุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี