[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Fw: System Information regarding automated theorem prover





On Sunday, 10 July 2016, 9:46, Moin Ud Deen <moinmalik07@xxxxxxxxx> wrote:




On Sunday, 10 July 2016, 9:43, Moin Ud Deen <moinmalik07@xxxxxxxxx> wrote:


Respected Sir,

i am studying MS computer science in UOS sargodha punjab pakistan.sir i need your little time, please kindly provide me access or details about the system regrading theorem prover which is developed under your nice supervision. i need this information for my subject formal method.
System General Information

Contributers

First appearance(date/year)

Latest version

Last Update

Web Address

Developed by (University/Industry)

License type

Unique Features

Main users Communities

Success stories


System Category

Type(Theorem Prover/Model Checker/)

Automated Theorem Prover ATP

Interactive Theorem Prover ITP/Proof assistant

Type w.r.t reasoning (Mathematical/Graphical )

Type w.r.t logic (FOL/HOL)

Type w.r.t Truth values ( Binary/Fuzzy/ Triadic/probabilistic/others)

Type w.r.t calculus (Deductive/Inductive)

Set theoretic support (ZF/ Fuzzy)

Paradigm (functional/ Imperative/ Other)



Programming framework

Language (C/C++/Java/Prolog/python/other)

User Interface (GUI/CLI)

Support (cross platform)

Scalability (Distributed/ Multi-threaded)

Architecture (modular/monolithic)

Debug Output/run time assertion

Inheritance/ OOP

Library

Standalone/Distributed

Code generation support


Internal framework

Small Proof kernel ( proof objects)

Extensible/programmable by the user

Editor support

Constructive logic supported?





Syntax:
-Syntax is inspired from which language? e.g. Haskell,ML,Java,C,C++...
-Either support available for Operator and Code? If aavilable then for which Operator and Coding scheme? e.g. infix/postfix/mixfix operators and unicode, Binary, ASCII.....
-unique feature according to syntax as compared to other?

Interactive Development or other process for program development

Tactic language available for writing proof or these are written by hand?

On which calculus and theory it is based on?

Proposition and set type?

Either it support inductive recursion?

What is the process of pattern matching?

Argument handling implicitly is available? Either it is heavy weight or light?

Either it allows to write non terminating program?

Either it is fixed and theoretically described system ? Or it is experimental and no descrption available for underlying theories?

Features provided in the system are more or less ? It is easier to learn or difficult based on these features?