มาติตา
ส่วนติดต่อผู้ใช้สำหรับการสร้างเอกสารพิสูจน์อักษร Matita
นักพัฒนา	ทีมมาติทา
ปล่อย	1999
เขียนเป็น	โอแคมล์
ระบบปฏิบัติการ	ลินุกซ์
มีจำหน่ายใน	ภาษาอังกฤษ
พิมพ์	การพิสูจน์ทฤษฎีบท
ใบอนุญาต	จีพีแอล
เว็บไซต์	http://matita.cs.unibo.itบนWayback Machine (เก็บถาวรเมื่อ 2023-02-04)

Matita ^{[ 1 ]} เป็นผู้ช่วยพิสูจน์ เชิงทดลอง ที่อยู่ระหว่างการพัฒนาที่ ภาควิชา วิทยาการคอมพิวเตอร์ของมหาวิทยาลัยโบโลญญาเป็นเครื่องมือที่ช่วยในการพัฒนาการพิสูจน์อย่างเป็นทางการโดยความร่วมมือระหว่างมนุษย์และเครื่องจักร โดยมีสภาพแวดล้อมการเขียนโปรแกรมที่ข้อกำหนดอย่างเป็นทางการ อัลกอริทึมที่สามารถดำเนินการได้ และใบรับรองความถูกต้องที่ตรวจสอบได้โดยอัตโนมัติสามารถอยู่ร่วมกันได้อย่างเป็นธรรมชาติ

Matita มีพื้นฐานมาจาก ระบบ ประเภทที่ขึ้นอยู่กันที่เรียกว่าแคลคูลัสของการสร้างแบบอุปนัยร่วม (ซึ่งเป็นอนุพันธ์ของแคลคูลัส ของการสร้าง ) และเข้ากันได้กับRocq ในระดับหนึ่ง

คำว่า "matita" หมายถึง "ดินสอ" ในภาษาอิตาลี (เครื่องมือแก้ไขที่เรียบง่ายและแพร่หลาย) เป็นแอปพลิเคชันขนาดเล็กและเรียบง่ายพอสมควร^{[ 2 ]}ซึ่งความซับซ้อนทางสถาปัตยกรรมและซอฟต์แวร์นั้นมีจุดประสงค์เพื่อให้ผู้เรียนสามารถใช้งานได้อย่างเชี่ยวชาญ โดยเป็นเครื่องมือที่เหมาะสมอย่างยิ่งสำหรับการทดสอบแนวคิดและโซลูชันที่เป็นนวัตกรรม Matita ใช้ โหมดการแก้ไขตาม กลยุทธ์ โดยวัตถุพิสูจน์ ( เข้ารหัส XML ) จะถูกสร้างขึ้นเพื่อการจัดเก็บและแลกเปลี่ยน

ตัวแปรเชิงการดำรงอยู่เป็นคุณสมบัติพื้นฐานใน Matita ซึ่งช่วยให้การจัดการเป้าหมายที่ขึ้นอยู่กันง่ายขึ้น^{[ 3 ]}

Matita ใช้ขั้นตอนวิธีอนุมานประเภทแบบ สองทิศทาง ^{[ 4 ]}โดยใช้ประโยชน์จากทั้งประเภทที่อนุมานและประเภทที่คาดหวัง

พลังของระบบอนุมานประเภท (ตัวปรับแต่ง) ได้รับการเสริมเพิ่มเติมด้วยกลไกคำแนะนำ^{[ 5 ]} ที่ช่วยในการสังเคราะห์ตัวรวมในสถานการณ์เฉพาะที่ผู้ใช้ระบุ

Matita รองรับกลยุทธ์การแยกความหมายที่ซับซ้อน^{[ 6 ]} โดยอาศัยการสนทนาระหว่างตัวแยกวิเคราะห์และตัวตรวจสอบประเภท

ในระดับการโต้ตอบ ระบบจะดำเนินการขั้นตอนเล็กๆ ของกลยุทธ์ที่มีโครงสร้าง^{[ 7 ]} ซึ่งช่วยให้การจัดการการพัฒนาการพิสูจน์ดีขึ้นมาก และนำไปสู่สคริปต์ที่มีโครงสร้างและอ่านง่ายยิ่งขึ้น

มาทิตาทำงานอยู่ที่CerCo (Certified Complexity) ซึ่งเป็น โครงการของสหภาพยุโรปภายใต้โครงการ FP7โดยมุ่งเน้นการพัฒนาคอมไพเลอร์ที่ได้รับการตรวจสอบอย่างเป็นทางการและรักษาความซับซ้อนไว้จากชุดย่อยขนาดใหญ่ของภาษาCไปยังภาษาแอสเซมบลีของไมโครโปรเซสเซอร์ MCS-51

บทช่วยสอน Matita ^{[ 8 ]}ให้คำแนะนำเชิงปฏิบัติเกี่ยวกับฟังก์ชันหลักของโปรแกรมพิสูจน์ทฤษฎีบทแบบโต้ตอบ Matita โดยนำเสนอการแนะนำผ่านชุดตัวอย่างที่ไม่ธรรมดาในด้าน การกำหนดคุณสมบัติ และการตรวจสอบ ซอฟต์แวร์

• การติดต่อสื่อสารระหว่างเคอร์รีและโฮเวิร์ด
• การพิสูจน์ทฤษฎีบทแบบโต้ตอบ
• ทฤษฎีประเภทสัญชาตญาณนิยม
• รายชื่อผู้ช่วยพิสูจน์อักษร

• โปรแกรมช่วยพิสูจน์อักษร MatitaบนWayback Machine (เก็บถาวรเมื่อ 2023-02-04)
• โครงการ CerCoในWayback Machine (เก็บถาวรเมื่อ 21 พฤษภาคม 2022)