Zobrazeno 1 - 10
of 1 256
pro vyhledávání: '"hol light"'
Autor:
Maggesi, Marco, Brogi, Cosimo Perini
Publikováno v:
Journal of Automated Reasoning 67.3 (2023): 29
We introduce our implementation in HOL Light of the metatheory for G\"odel-L\"ob provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we
Externí odkaz:
http://arxiv.org/abs/2205.03659
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
EPTCS 332, 2021, pp. 18-34
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive forward and back
Externí odkaz:
http://arxiv.org/abs/2101.03808
We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type theory that
Externí odkaz:
http://arxiv.org/abs/1802.00405
Autor:
Rashid, Adnan, Hasan, Osman
The Laplace transform is an algebraic method that is widely used for analyzing physical systems by either solving the differential equations modeling their dynamics or by evaluating their transfer function. The dynamics of the given system are firstl
Externí odkaz:
http://arxiv.org/abs/1806.03049
Conference
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Rashid, Adnan, Hasan, Osman
Transform methods, like Laplace and Fourier, are frequently used for analyzing the dynamical behaviour of engineering and physical systems, based on their transfer function, and frequency response or the solutions of their corresponding differential
Externí odkaz:
http://arxiv.org/abs/1705.10050
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming August 2019 106:29-38
Autor:
Gauthier, Thibault, Kaliszyk, Cezary
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper w
Externí odkaz:
http://arxiv.org/abs/1509.03527
Autor:
Carneiro, Mario
We present an algorithm for converting proofs from the OpenTheory interchange format, which can be translated to and from any of the HOL family of proof languages (HOL4, HOL Light, ProofPower, and Isabelle), into the ZFC-based Metamath language. This
Externí odkaz:
http://arxiv.org/abs/1412.8091