Some Research Issues in Higher Order Logic Theorem Proving

Some Research Issues in Higher Order Logic Theorem Proving

Sonraí bibleagrafaíochta
Príomhchruthaitheoir:	Melham, T
Formáid:	Report
Foilsithe / Cruthaithe:	Department of Computer Science‚ University of Aarhus 1996

Míreanna comhchosúla

Introduction to HOL: A theorem proving environment for higher order logic
Foilsithe / Cruthaithe: (1993)

Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems
de réir: Zheng Yang, et al.
Foilsithe / Cruthaithe: (2018-01-01)

Some observations on the logical foundations of inductive theorem proving
de réir: Stefan Hetzl, et al.
Foilsithe / Cruthaithe: (2018-04-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
de réir: Adnan Rashid, et al.
Foilsithe / Cruthaithe: (2020-01-01)

Symbolic logic and mechanical theorem proving /
de réir: 336504 Chang, Chin-Ling, et al.
Foilsithe / Cruthaithe: (1973)

Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications
Foilsithe / Cruthaithe: (1994)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
de réir: Adnan Rashid, et al.
Foilsithe / Cruthaithe: (2022-06-01)

Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving
de réir: Aagaard, M, et al.
Foilsithe / Cruthaithe: (1999)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
de réir: Melham, T
Foilsithe / Cruthaithe: (2004)

Automated theorem proving : a logical basis /
de réir: 403272 Loveland, Donald W.
Foilsithe / Cruthaithe: (1978)

Higher Order Logic and Hardware Verification
de réir: Melham, T
Foilsithe / Cruthaithe: (1993)

A Study Of User Activity In Interactive Theorem Proving
de réir: Aitken, S, et al.
Foilsithe / Cruthaithe: (1995)

Interactive Theorem Proving: An Empirical Study of User Activity
de réir: Aitken, J, et al.
Foilsithe / Cruthaithe: (1998)

A Reflective Functional Language for Hardware Design and Theorem Proving
de réir: Grundy, J, et al.
Foilsithe / Cruthaithe: (2006)

A Reflective Functional Language for Hardware Design and Theorem Proving
de réir: Grundy, J, et al.
Foilsithe / Cruthaithe: (2003)

Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)
de réir: Aagaard, M, et al.
Foilsithe / Cruthaithe: (2000)

A Human Oriented Logic for Automatic Theorem Proving
de réir: Nevins, Arthur J.
Foilsithe / Cruthaithe: (2004)

Logic for computer science : foundations of automatic theorem proving /
de réir: 455116 Gallier, Jean H.
Foilsithe / Cruthaithe: (1986)

Conditional and preferential logics : proof methods and theorem proving /
de réir: 518526 Pozzato, Gian Luca
Foilsithe / Cruthaithe: (c201)

Automating Recursive Type Definitions in Higher Order Logic
de réir: Melham, T
Foilsithe / Cruthaithe: (1989)

Automating Recursive Type Definitions in Higher Order Logic
de réir: Melham, T
Foilsithe / Cruthaithe: (1988)

Formalization of Linear Space Theory in the Higher-Order Logic Proving System
de réir: Jie Zhang, et al.
Foilsithe / Cruthaithe: (2013-01-01)

Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
de réir: O'Leary, J, et al.
Foilsithe / Cruthaithe: (2013)

Relational STE and theorem proving for formal verification of industrial circuit designs
de réir: O'Leary, J, et al.
Foilsithe / Cruthaithe: (2013)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
de réir: Melham, T
Foilsithe / Cruthaithe: (1989)

ProoFVer: Natural Logic Theorem Proving for Fact Verification
de réir: Amrith Krishna, et al.
Foilsithe / Cruthaithe: (2022-01-01)

Translating Dependent Type Theory into Higher Order Logic
de réir: Jacobs, B, et al.
Foilsithe / Cruthaithe: (1993)

Hardware Verification using Higher−Order Logic
de réir: Camilleri, A, et al.
Foilsithe / Cruthaithe: (1986)

Hardware Verification using Higher−Order Logic
de réir: Camilleri, A, et al.
Foilsithe / Cruthaithe: (1987)

Using Recursive Types to Reason about Hardware in Higher Order Logic
de réir: Melham, T
Foilsithe / Cruthaithe: (1988)

Using Recursive Types to Reason about Hardware in Higher Order Logic
de réir: Melham, T
Foilsithe / Cruthaithe: (1988)

Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings
Foilsithe / Cruthaithe: (2005)

Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta‚ Malta‚ September 19–22‚ 1994: Proceedings
Foilsithe / Cruthaithe: (1994)

Theorem proving [filem]
Foilsithe / Cruthaithe: (1969)

Theorem proving [kasetvideo]
Foilsithe / Cruthaithe: (1969)

Theorem proving for prenex G\"odel logic with Delta: checking validity and unsatisfiability
de réir: Matthias Baaz, et al.
Foilsithe / Cruthaithe: (2012-03-01)

Theorem Proving in Higher Order Logics [electronic resource] : 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007: Proceedings /
de réir: TPHOLs 2007 (2007 : Kaiserslautern, Germany), et al.
Foilsithe / Cruthaithe: (2007)

Elementary Geometry Theorem Proving
de réir: Goldstein, Ira
Foilsithe / Cruthaithe: (2004)

Playing with LEGO and proving theorems
de réir: Tanswell, FS
Foilsithe / Cruthaithe: (2017)

PLANNER: A Language for Proving Theorems
de réir: Hewitt, Carl
Foilsithe / Cruthaithe: (2004)