Structuring and automating hardware proofs in a higher-order theorem-proving environment

1993 ◽  
Vol 2 (2) ◽  
pp. 165-223 ◽  
Author(s):  
Ramayya Kumar ◽  
Klaus Schneider ◽  
Thomas Kropf
Keyword(s):  
Theorem Proving ◽  
Higher Order

scholarly journals Higher-order theorem proving and its applications

2019 ◽  
Vol 61 (4) ◽  
pp. 187-191
Author(s):  
Alexander Steen
Keyword(s):  
Theorem Proving ◽  
Formal Analysis ◽  
Logical Consequence ◽  
Effective Means ◽  
Industrial Applications ◽  
Higher Order ◽  
Hardware Verification ◽  
Theorem Prover ◽  
Computer Assisted ◽  
Higher Order Logic

Abstract Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.

Comparing Approaches To Resolution Based Higher-Order Theorem Proving

Synthese ◽  
2002 ◽  
Vol 133 (1/2) ◽  
pp. 203-235 ◽  
Author(s):  
Christoph Benzmüller
Keyword(s):  
Theorem Proving ◽  
Higher Order
Sign in / Sign up

Export Citation Format

Share Document