標(biāo)題: Titlebook: Higher Order Logic Theorem Proving and Its Applications; 6th International Wo Jeffrey J. Joyce,Carl-Johan H. Seger Conference proceedings 1 [打印本頁] 作者: 浮淺 時間: 2025-3-21 18:41
書目名稱Higher Order Logic Theorem Proving and Its Applications影響因子(影響力)
書目名稱Higher Order Logic Theorem Proving and Its Applications影響因子(影響力)學(xué)科排名
書目名稱Higher Order Logic Theorem Proving and Its Applications網(wǎng)絡(luò)公開度
書目名稱Higher Order Logic Theorem Proving and Its Applications網(wǎng)絡(luò)公開度學(xué)科排名
書目名稱Higher Order Logic Theorem Proving and Its Applications被引頻次
書目名稱Higher Order Logic Theorem Proving and Its Applications被引頻次學(xué)科排名
書目名稱Higher Order Logic Theorem Proving and Its Applications年度引用
書目名稱Higher Order Logic Theorem Proving and Its Applications年度引用學(xué)科排名
書目名稱Higher Order Logic Theorem Proving and Its Applications讀者反饋
書目名稱Higher Order Logic Theorem Proving and Its Applications讀者反饋學(xué)科排名
作者: 神秘 時間: 2025-3-21 22:09
Mechanizing a programming logic for the concurrent programming language microSR in HOL,en to be sound within HOL. The logic we derived allows one to reason and state formal assertions about concurrently executing processes that do not share any data objects, but communicate through shared channels.作者: TAIN 時間: 2025-3-22 00:29
Reasoning with the formal definition of standard ML in HOL, The correctness of the representation is demonstrated by the derivation of several important language properties, including determinacy. A symbolic evaluator to assist in proving properties of Standard ML program fragments is also described. Some sample applications of the theory in the area of program verification are given.作者: Vldl379 時間: 2025-3-22 05:33 作者: 朋黨派系 時間: 2025-3-22 12:31
The HOL-Voss system: Model-checking inside a general-purpose theorem-prover,pproach. We illustrate the use of this extension with three examples, namely, the formal verification of a 32-bit adder, an 8-bit by 8-bit multiplier and the MAJORLOGIC block of the Viper microprocessor.作者: decipher 時間: 2025-3-22 16:31 作者: 元音 時間: 2025-3-22 17:35 作者: FOLLY 時間: 2025-3-22 21:39 作者: 驚奇 時間: 2025-3-23 03:20
0302-9743 s 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove".978-3-540-57826-0978-3-540-48346-5Series ISSN 0302-9743 Series E-ISSN 1611-3349 作者: 低位的人或事 時間: 2025-3-23 09:09 作者: caldron 時間: 2025-3-23 13:00
A functional approach for formalizing regular hardware structures,ut on regular hardware structures which are described by means of primitive recursion. PML-descriptions can easily be converted to syntactic structures, called hardware formulae, which can then be verified by the MEPHISTO system.作者: 粗俗人 時間: 2025-3-23 15:50
Alternative proof procedures for finite-state machines in higher-order logic,entable proof methods which do not use knowledge of fixpoint theorems are given. Since these methods are incomplete, the second category exploits an external program for computing fixpoint lemmata which can then be easily proved in HOL.作者: Aggrandize 時間: 2025-3-23 20:50
A formalization of abstraction in LAMBDA,model only if they are satisfied in the model itself. We illustrate how the proof of an inductive step in the verification of a satisfaction relation for an infinite model can be reduced to the verification of a satisfaction relation for a very small finite model.作者: cavity 時間: 2025-3-23 22:46
Report on the UCD microcoded Viper verification project, We redesigned Viper as a hierarchy of five interpreters, each of which is an instance of the generic interpreter. The top level specifies the Viper instruction set and the lowest level specifies an abstraction of a conventional electronic block model. The design and verification was carried out in approximately one person-year.作者: 江湖郎中 時間: 2025-3-24 04:34
0302-9743 umbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contain作者: LANCE 時間: 2025-3-24 10:30
978-3-540-57826-0Springer-Verlag Berlin Heidelberg 1994作者: 小蟲 時間: 2025-3-24 13:27
Higher Order Logic Theorem Proving and Its Applications978-3-540-48346-5Series ISSN 0302-9743 Series E-ISSN 1611-3349 作者: Introduction 時間: 2025-3-24 18:06 作者: 噱頭 時間: 2025-3-24 21:36
https://doi.org/10.1007/3-540-57826-9Automatisches Beweisen; Hardwareverifikation; Higher Order Logic System (HOL); Higher-Order-Logic Syste作者: 過剩 時間: 2025-3-24 23:43
Structure and behaviour in hardware verification,In this paper we review how hardware has been described in the formal hardware verification community. Recent developments in hardware description are evaluated against the background of the use of hardware description languages, and also in relation to programming languages. The notions of structure and behaviour are crucial to this discussion.作者: HPA533 時間: 2025-3-25 04:58
A proof development system for the HOL theorem prover,In this paper, we present a system to improve the interaction between HOL and the user when doing proofs.作者: Mobile 時間: 2025-3-25 09:37 作者: 解凍 時間: 2025-3-25 14:01
Some theorems we should prove,Mathematical techniques can be used to produce precise, provably complete documentation for computer systems. However, such documents are highly detailed; oversights and other errors arc quite common. To detect the “early” errors in a document, one must attempt to prove certain simple theorems. This paper gives some examples of such theorems.作者: obsolete 時間: 2025-3-25 18:44
Using PVS to prove some theorems of David Parnas,David Parnas [13] describes some theorems representative of those encountered in support of certification of software for the Darlington nuclear reactor. We describe the verification of these theorems using PVS.作者: 圣歌 時間: 2025-3-25 23:40
Extending the HOL theorem prover with a computer algebra system to reason about the reals,In this paper we describe an environment for reasoning about the reals which combines the rigour of a theorem prover with the power of a computer algebra system.作者: CROW 時間: 2025-3-26 01:45 作者: 止痛藥 時間: 2025-3-26 08:15 作者: 種族被根除 時間: 2025-3-26 11:18 作者: 戲服 時間: 2025-3-26 12:45
Reasoning with the formal definition of standard ML in HOL,. HOL theories of the Core syntax and dynamic semantics are presented, including a purely definitional representation of the semantic inference rules. The correctness of the representation is demonstrated by the derivation of several important language properties, including determinacy. A symbolic e作者: 不安 時間: 2025-3-26 18:14 作者: 使乳化 時間: 2025-3-27 00:04
Degrees of formality in shallow embedding hardware description languages in HOL,complex issues than it was possible or practically feasible in the past. It is often the case that a model of a system is built in a formal logic and then reasoning about this model is carried out in the logic. Concern is growing on how to consistently interface a model built in a formal logic with 作者: ROOF 時間: 2025-3-27 04:08 作者: PATRI 時間: 2025-3-27 05:20 作者: 故意 時間: 2025-3-27 11:41 作者: 正論 時間: 2025-3-27 15:41 作者: NORM 時間: 2025-3-27 21:40
Alternative proof procedures for finite-state machines in higher-order logic,on procedures for this logic or finite-state machines is however not very easy within the HOL system, since it requires the proof of certain fixpoint theorems and a creation of a new theory based on it. The main contribution of this paper is to give some alternative proof procedures so that proof ta作者: 偉大 時間: 2025-3-28 00:10
A formalization of abstraction in LAMBDA,y models by considering abstract versions of them. We report on work in progress that aims to develop support within LAMBDA for a systematic approach to abstraction. We give a formalization in LAMBDA of a notion of abstraction for transition systems; the abstract systems have two sorts of transition作者: MAPLE 時間: 2025-3-28 04:02
Report on the UCD microcoded Viper verification project, (mostly because it became too time consuming) is of particular interest. Our view of the incomplete proof is that the jump in abstraction between the electronic block model and the specification is too great. By introducing intermediate levels between the two extreme models, the overall proof becom作者: 鉗子 時間: 2025-3-28 09:16 作者: 冥界三河 時間: 2025-3-28 14:27
Flemming Andersen,Kim Dam Petersen,Jimmi S. Petterssonr a competitive economy.. The case where no equilibrium exists even though indifference curves, production functions, and so on, are fairly well behaved is a useful one to show the necessity of proving the existence of equilibrium. Mill (1869) indicates that one of the first examples of the non-exis作者: BADGE 時間: 2025-3-28 18:30 作者: insomnia 時間: 2025-3-28 20:35 作者: LUT 時間: 2025-3-29 00:59
Donald Symer a competitive economy.. The case where no equilibrium exists even though indifference curves, production functions, and so on, are fairly well behaved is a useful one to show the necessity of proving the existence of equilibrium. Mill (1869) indicates that one of the first examples of the non-exis作者: AGATE 時間: 2025-3-29 05:16 作者: motivate 時間: 2025-3-29 10:48 作者: Flinch 時間: 2025-3-29 15:25 作者: Expiration 時間: 2025-3-29 17:41 作者: 表否定 時間: 2025-3-29 22:52 作者: Sarcoma 時間: 2025-3-30 00:42 作者: 脫毛 時間: 2025-3-30 07:25
Jeffrey Joyce,Carl Segerionship between Aristotle’s and Cicero’s work on topoi.Offer.Ars Topica. is the first full-length study of the nature and development of .topoi., the conceptual ancestors of modern argument schemes, between Aristotle and Cicero...Aristotle and Cicero configured .topoi. in a way that influenced the s作者: 從屬 時間: 2025-3-30 09:49
Juin-Yeu Lu,Shiu-Kai Chinionship between Aristotle’s and Cicero’s work on topoi.Offer.Ars Topica. is the first full-length study of the nature and development of .topoi., the conceptual ancestors of modern argument schemes, between Aristotle and Cicero...Aristotle and Cicero configured .topoi. in a way that influenced the s作者: 信任 時間: 2025-3-30 13:27 作者: Nonthreatening 時間: 2025-3-30 19:08
Anthony McIsaacionship between Aristotle’s and Cicero’s work on topoi.Offer.Ars Topica. is the first full-length study of the nature and development of .topoi., the conceptual ancestors of modern argument schemes, between Aristotle and Cicero...Aristotle and Cicero configured .topoi. in a way that influenced the s作者: fiscal 時間: 2025-3-30 21:54 作者: 柱廊 時間: 2025-3-31 01:05 作者: agitate 時間: 2025-3-31 06:20
Kim Dam Petersenuilibrium failed because of their assumption of continuity. The Thornton-Mill examples, as well as the example of Wald (1951), are, however, not so serious to equilibrium theory, if we consider, not the Walrasian . with recontract, but the non-. without recontract. From such non-. point of view, a t作者: 攤位 時間: 2025-3-31 10:25
Cui Zhang,Rob Shaw,Ronald A. Olsson,Karl Levitt,Myla Archer,Mark R. Heckman,Gregory D. Bensonuilibrium failed because of their assumption of continuity. The Thornton-Mill examples, as well as the example of Wald (1951), are, however, not so serious to equilibrium theory, if we consider, not the Walrasian . with recontract, but the non-. without recontract. From such non-. point of view, a t作者: nonradioactive 時間: 2025-3-31 16:35 作者: 細節(jié) 時間: 2025-3-31 19:18
Myra Vanlnwegen,Elsa Gunteruilibrium failed because of their assumption of continuity. The Thornton-Mill examples, as well as the example of Wald (1951), are, however, not so serious to equilibrium theory, if we consider, not the Walrasian . with recontract, but the non-. without recontract. From such non-. point of view, a t作者: integral 時間: 2025-3-31 22:56
