1 |
Mechanising heterogeneous reasoning in theorem proversUrbas, Matej January 2014 (has links)
No description available.
|
2 |
Generating pseudo-random theorems for testing theorem proversDarwish, Nevin Mahmoud, 1952- January 1978 (has links)
No description available.
|
3 |
Hyperresolution for resolution logicsGhazizadeh, Behrad. January 1999 (has links)
Thesis (M. Sc.)--York University, 1999. Graduate Programme in Computer Science. / Typescript. Includes bibliographical references (leaves 76-77). Also available on the Internet. MODE OF ACCESS via web browser by entering the following URL: http://wwwlib.umi.com/cr/yorku/fullcit?pMQ39193.
|
4 |
Generating pseudo-random theorems for testing theorem proversDarwish, Nevin Mahmoud, 1952- January 1978 (has links)
No description available.
|
5 |
A unit resolution theorem proving systemLeQuesne, Peter Neave January 1972 (has links)
A unit resolution theorem proving system is developed and compared with the previous work of C.L. Chang. This thesis includes a description of a particular approach to unit resolution and a description of the resulting program and its effectiveness. / Science, Faculty of / Computer Science, Department of / Graduate
|
6 |
On the completeness of linear strategies in automatic consequence findingMinicozzi, Eliana January 1972 (has links)
The problem of the automatic generation of logical consequences of a set of axioms is examined. The merging subsumption linear strategy has been shown complete with respect to that problem. A generalization of a set of support strategy is given, and the completeness of merging subsumption linear strategy with set of support is proved. The merging-linear-A-ordered strategy and the merging linear-C-ordered strategy have been shown to be incomplete. Relations between unit strategy and input strategy have been examined. A little review of the ‘interesting theorem’ is given. / Science, Faculty of / Computer Science, Department of / Graduate
|
7 |
An analysis of Specware and its usefulness in the verification of high assurance systemsDeCloss, Daniel P. 06 1900 (has links)
Formal verification is required for systems that require high assurance. Formal verification can require large and complex proofs that can drastically affect the development life cycle. Through the use of a verification system, such proofs can be managed and completed in an efficient manner. A verification system consists of a specification language that can express formal logic, and an automated theorem tool that can be used to verify theorems and conjectures within the specifications. One example of a verification system is Specware. This thesis presents an analysis of Specware against a set of evaluation criteria in order to determine the level of usefulness Specware can have in the verification of high assurance systems. This analysis revealed that Specware contains a powerful specification language capable of representing higher order logic in a simple and expressive manner. Specware is able to represent multiple levels of abstraction and generate proof obligations regarding specification correctness and interlevel mapping. The theorem prover associated with Specware was found to be lacking in capability. Through this analysis we found that Specware has great potential to be an excellent verification system given improvement upon the theorem prover and strengthening of weaknesses regarding linguistic components. / Naval Postgraduate School author (civilian).
|
8 |
Transparency in formal proof /Petschulat, Cap. January 2009 (has links)
Thesis (M.S.)--Boise State University, 2009. / Includes abstract. Includes bibliographical references (leaves 52-53).
|
9 |
Transparency in formal proofPetschulat, Cap. January 2009 (has links)
Thesis (M.S.)--Boise State University, 2009. / Title from t.p. of PDF file (viewed June 15, 2010). Includes abstract. Includes bibliographical references (leaves 52-53).
|
10 |
Algorithmic applications of propositional proof complexity /Sabharwal, Ashish, January 2005 (has links)
Thesis (Ph. D.)--University of Washington, 2005. / Vita. Includes bibliographical references (p. 155-165).
|
Page generated in 0.0923 seconds