数理逻辑在计算机科学中的应用：系统建模与推理

5星 · 超过95%的资源需积分: 42 135 浏览量更新于2024-07-26 收藏 2.13MB PDF 举报

"面向计算机科学的数理逻辑系统建模与推理" 本书《面向计算机科学的数理逻辑系统建模与推理》由Michael Huth和Mark Ryan合著，来自英国伦敦帝国学院计算系和伯明翰大学计算机科学学院的专家共同撰写。这本书深入探讨了数理逻辑在计算机科学中的应用，特别是系统建模和推理方面。书中涵盖的内容广泛，旨在帮助读者理解和运用数理逻辑工具解决实际的计算机科学问题。数理逻辑是计算机科学基础的重要组成部分，它涉及形式逻辑系统、证明理论和模型理论等。在本书中，作者可能详细介绍了以下知识点： 1. 形式语言：包括命题逻辑和一阶逻辑，以及它们的语法和语义。这些基础知识对于理解逻辑表达式的构造和含义至关重要。 2. 证明理论：讨论如何构造和验证逻辑推理，如自然演绎系统、归结法（resolution）和sequent calculus等证明方法。这有助于理解程序正确性的验证。 3. 模型理论：研究逻辑公式在结构（模型）中的满足性，如Tarski的真度定义和同构理论，这对于理解数据结构和算法的性质很有帮助。 4. 逻辑与计算：介绍逻辑与计算复杂性理论的关系，例如逻辑可判定性问题和递归理论，这与计算过程的效率和可行性有关。 5. 代数逻辑：探讨代数方法在逻辑中的应用，如布尔代数和克林逻辑，这些在数据库查询和并发系统中有着广泛的应用。 6. 逻辑在系统建模中的应用：可能涵盖了Z规格说明语言、B方法和其他形式化建模技术，这些都是系统设计和验证的有效工具。 7. 证明助手和自动定理证明：介绍如何利用计算机辅助工具（如Isabelle, Coq等）进行形式证明，这对于自动化推理和软件验证非常重要。 8. 逻辑与编程语言：讨论逻辑编程语言如Prolog，以及函数式编程语言与逻辑的联系，如lambda演算和 Curry-Howard 同构。 9. 逻辑与并发：在分布式系统和多线程编程中，同步和通信的逻辑模型，如Hoare逻辑和Lamport逻辑，用于分析并发行为的正确性。 10. 实例与案例研究：书中可能包含实际问题的案例分析，以展示如何将数理逻辑应用于具体计算机系统的分析和设计。通过阅读本书，读者可以深入理解数理逻辑在计算机科学中的核心地位，并能够将其应用于系统建模、验证和推理中，提升软件开发的质量和可靠性。此外，书中可能还包括练习题和习题，以帮助读者巩固所学知识并提升问题解决能力。尽管没有提供具体内容，但这些主题的全面覆盖确保了对计算机科学中数理逻辑的深入学习。

xiv Acknowledgements

we mention Wolfgang Ahrendt, Yasuhiro Ajiro, Torben Amtoft, Stephan

Andrei, Bernhard Beckert, Jonathan Brown, James Caldwell, Ruchira Datta,

Amy Felty, Dimitar Guelev, Hirotsugu Kakugawa, Kamran Kashef, Markus

Kr¨otzsch, Jagun Kwon, Ranko Lazic, David Makinson, Alexander Miczo,

Aart Middeldorp, Robert Morelli, Prakash Panangaden, Aileen Paraguya,

Frank Pfenning, Shekhar Pradhan, Koichi Takahashi, Kazunori Ueda,

Hiroshi Watanabe, Fuzhi Wang and Reinhard Wilhelm.

2 1Propositional logic

done is substituted some sentence fragments for others:

Example 1.1

Example 1.2

the train is late it is raining

there are taxis at the station

Jane has her umbrella with her

John is late for his meeting

Jane gets wet.

The argument in each example could be stated without talking about trains

and rain, as follows:

If p and not q,then r.Notr. p. Therefore, q.

In developing logics, we are not concerned with what the sentences really

mean, but only in their logical structure. Of course, when we apply such

reasoning, as done above, such meaning will be of great interest.

1.1 Declarative sentences

In order to make arguments rigorous, we need to develop a language in which

we can express sentences in such a way that brings out their logical structure.

The language we begin with is the language of propositional logic. It is based

on propositions,ordeclarative sentences which one can, in principle, argue

as being true or false. Examples of declarative sentences are:

(1) The sum of the numbers 3 and 5 equals 8.

(2) Jane reacted violently to Jack’s accusations.

(3) Every even natural number >2isthesumoftwoprime numbers.

(4) All Martians like pepperoni on their pizza.

(5) Albert Camus ´etait un ´ecrivain fran¸cais.

(6) Die W¨urde des Menschen ist unantastbar.

These sentences are all declarative, because they are in principle capable of

being declared ‘true’, or ‘false’. Sentence (1) can be tested by appealing to

basic facts about arithmetic (and by tacitly assuming an Arabic, decimal

representation of natural numbers). Sentence (2) is a bit more problematic.

In order to give it a truth value, we need to know who Jane and Jack are

and perhaps to have a reliable account from someone who witnessed the

situation described. In principle, e.g., if we had been at the scene, we feel

that we would have been able to detect Jane’s violent reaction, provided

that it indeed occurred in that way. Sentence (3), known as Goldbach’s

conjecture, seems straightforward on the face of it. Clearly, a fact about

all even numbers >2iseithertrue or false. But to this day nobody knows

whether sentence (3) expresses a truth or not. It is even not clear whether

this could be shown by some ﬁnite means, even if it were true. However, in

1.1 Declarative sentences 3

this text we will be content with sentences as soon as they can, in principle,

attain some truth value regardless of whether this truth value reﬂects the

actual state of aﬀairs suggested by the sentence in question. Sentence (4)

seems a bit silly, although we could say that if Martians exist and eat pizza,

then all of them will either like pepperoni on it or not. (We have to introduce

predicate logic in Chapter 2 to see that this sentence is also declarative if no

Martians exist; it is then true.) Again, for the purposes of this text sentence

(4) will do. Et alors, qu’est-ce qu’on pense des phrases (5) et (6)? Sentences

(5) and (6) are ﬁne if you happen to read French and German a bit. Thus,

declarative statements can be made in any natural, or artiﬁcial, language.

The kind of sentences we won’t consider here are non-declarative ones,

Could you please pass me the salt?

Ready, steady, go!

May fortune come your way.

Primarily, we are interested in precise declarative sentences, or statements

about the behaviour of computer systems, or programs. Not only do we

want to specify such statements but we also want to check whether a given

program, or system, fulﬁls a speciﬁcation at hand. Thus, we need to develop

acalculus of reasoning which allows us to draw conclusions from given as-

sumptions, like initialised variables, which are reliable in the sense that they

preserve truth: if all our assumptions are true, then our conclusion ought to

be true as well. A much more diﬃcult question is whether, given any true

property of a computer program, we can ﬁnd an argument in our calculus

that has this property as its conclusion. The declarative sentence (3) above

might illuminate the problematic aspect of such questions in the context of

number theory.

The logics we intend to design are symbolic in nature. We translate a cer-

tain suﬃciently large subset of all English declarative sentences into strings

of symbols. This gives us a compressed but still complete encoding of declar-

ative sentences and allows us to concentrate on the mere mechanics of our

argumentation. This is important since speciﬁcations of systems or software

are sequences of such declarative sentences. It further opens up the possibil-

ity of automatic manipulation of such speciﬁcations, a job that computers

just love to do

.Our strategy is to consider certain declarative sentences as

There is a certain, slightly bitter, circularity in such endeavours: in proving that a certain

computer program P satisﬁes a given property, we might let some other computer program Q try

to ﬁnd a proof that P satisﬁes the property; but who guarantees us that Q satisﬁes the property

of producing only correct proofs? We seem to run into an inﬁnite regress.

4 1Propositional logic

being atomic,orindecomposable, like the sentence

‘The number 5 is even.’

We assign certain distinct symbols p, q, r,...,orsometimes p

,... to

each of these atomic sentences and we can then code up more complex

sentences in a compositional way. For example, given the atomic sentences

p:‘Iwon the lottery last week.’

q:‘Ipurchased a lottery ticket.’

r:‘Iwon last week’s sweepstakes.’

we can form more complex sentences according to the rules below:

¬:Thenegation of p is denoted by ¬p and expresses ‘I did not win the lottery

last week,’ or equivalently ‘It is not true that I won the lottery last week.’

∨:Givenp and r we may wish to state that at least one of them is true: ‘I won the

lottery last week, or Iwon last week’s sweepstakes;’ we denote this declarative

sentence by p ∨r and call it the disjunction of p and r

∧:Dually, the formula p ∧ r denotes the rather fortunate conjunction of p and r:

‘Last week I won the lottery and the sweepstakes.’

→:Last, but deﬁnitely not least, the sentence ‘If Iwon the lottery last week,

then I purchased a lottery ticket.’ expresses an implication between p and q,

suggesting that q is a logical consequence of p.Wewrite p → q for that

.We

call p the assumption of p → q and q its conclusion.

Of course, we are entitled to use these rules of constructing propositions

repeatedly. For example, we are now in a position to form the proposition

p ∧ q →¬r ∨ q

which means that ‘if p and q then not r or q’. You might have noticed a

potential ambiguity in this reading. One could have argued that this sentence

has the structure ‘p is the case and if q then . ..’Acomputer would require

the insertion of brackets, as in

(p ∧ q) → ((¬r) ∨ q)

Its meaning should not be confused with the often implicit meaning of or in natural language

discourse as either ...or.Inthistextor always means at least one of them and should not be

confounded with exclusive or which states that exactly one of the two statements holds.

The natural language meaning of ‘if ...then ...’ often implicitly assumes a causal role of

the assumption somehow enabling its conclusion. The logical meaning of implication is a bit

diﬀerent, though, in the sense that it states the preservation of truth which might happen

without any causal relationship. For example, ‘If all birds can ﬂy, then Bob Dole was never

president of the United States of America.’ is a true statement, but there is no known causal

connection between the ﬂying skills of penguins and eﬀective campaigning.

剩余442页未读，继续阅读

starry225

粉丝: 0
资源: 1

数理逻辑在计算机科学中的应用：系统建模与推理

计算机科学的数理逻辑 、系统建模与推理的答案

面向计算机科学的数理逻辑习题答案

面向计算机科学的数理逻辑(PDF:陆钟万)

面向计算机科学的数理逻辑系统建模与推理 答案 csdn

面向计算机科学的数理逻辑 系统建模与推理（全部） 答案

面向计算机科学的数理逻辑:系统建模与推理(英文版)

面向计算机科学的数理逻辑:系统建模与推理pdf

面向计算机科学的数理逻辑系统与建模1-2章课后习题答案

面向计算机的数理逻辑

面向计算机科学的数理逻辑课后习题答案

最新资源

计算机科学的数理逻辑、系统建模与推理的答案

面向计算机科学的数理逻辑系统建模与推理答案 csdn

面向计算机科学的数理逻辑系统建模与推理（全部）答案