SC Chapter 1 Introduction

Questions about the lecture 'From Molecular to Continuum Physics 1' of the RWTH Aachen Chapter 1 Introduction

Questions about the lecture 'From Molecular to Continuum Physics 1' of the RWTH Aachen Chapter 1 Introduction


Fichier Détails

Cartes-fiches 32
Langue English
Catégorie Informatique
Niveau Université
Crée / Actualisé 18.02.2017 / 18.02.2017
Lien de web
https://card2brain.ch/box/20170218_sc_chapter_1_introduction
Intégrer
<iframe src="https://card2brain.ch/box/20170218_sc_chapter_1_introduction/embed" width="780" height="150" scrolling="no" frameborder="0"></iframe>

What are the components of satisfiability checking? [3]

1. Quantifier-free logical formula

2. Solver

3. Satisfiability of the input formula

What is the problem of quantifier-free logical formula?

How to specify input into a formula?

What is the problem of the solver?

How to solve the formula?

What is the problem of the satisfiability of the input formula?

How to specify output of satisfiability

What is a logical systems?

Framework for inference and correct reasoning

What is syntax? [2]

1. Form of logical formulas with axioms and inference rules

2. Combination of atomic propositions or constraints using boolean operators (and, or, not)

What is semantic? [2]

1. Structure derives and gives meaning to logical formulas

2. Substitute truth values or type correct for propositions such that the formula evaluates to true

What is the problem of substitution?

Hard or even undecidable (non-linear integer arithmetic)

What are characteristics of logical systems? [3]

1. Consistency, 2. soundness and 3. completeness

Which logic dominated from 500 B.C. to 19th century?

Philosophical logic

Which logic dominated from Mid 19th century to late 19th century?

Symbolic logic

Which logic dominated from late 19th century to mid 20th century?

Mathematical logic

Which logic dominates today

Computer science logic

What are the characteristics of philosophical logic?

1. Natural language sentences used by humans

2. Ambiguous and 13 types of fallacies by Aristotle in “Sophistical Refutations

Name six fallacies of by Aristotle? [6]

1. Composition

2. Division

3. Figure of speech

4. Affirming the consequent

5. Inconsistency

6. Conjunction

What is problem of the fallacy composition?

One part is true, therefor the whole is true

A and A part of B therefor B

What is problem of the fallacy division?

Truths of things are also truths for subparts

B and A part of B therefor A

What is problem of the fallacy figure of speech?

Change the usual meaning of words

What is problem of the fallacy affirming the consequent?

Because of the consequent the origin is true too

A → B and B therefor A

What is problem of the fallacy affirming the inconsistency?

“This sentence is a lie” (The liar’s paradox)

What is problem of the fallacy affirming the conjunction?

Combination of two statements is not working as expected

“This sentence has five words” therefor “This sentence has five words and this sentence has five words”

What happened 1854?

Boole with Boolean logic

What happened 1879

Frege with modern logic in Begriffsschrift using quantifier notation

What happened from 1910 to 1913?

Whitehead and Russell with Principia Mathematica and deriving mathematical truths from axioms

What happened 1931?

Gödel and Turing with undecidability results

Which logics exist today? [4]

1. Propositional logic

2. First order logic

3. Higher order logic

4. Temporal logic

What is the problem of propositional logic?

Sometimes too weak for modeling

What are areas for computer science logic? [3]

1. Databases

2. Programming languages // Prolog

3. Specification and verification

Which subcategories of satisfiability checking exist? [3]

1. Symbolic computation

2. Propositional logic (SAT)

3. SAT modulo theories (SMT)

What are facts about SAT solving? [2]

1. Used in research and industry

2. Community support with benchmarks and competitions

What are applications of SAT solving? [10]

1. Hardware verification

2. Symbolic execution

3. Bounded model checking // for C/C++ and graph transformation systems

4. Termination analysis for programs // Term rewrite system (TRS) → Dependency pairs → Chains

5. jUnit_RV for runtimme verification of multi-threaded, object-oriented systems

6. Planning

7. Scheduling

8. Development optimization on the cloud

9. Parameter synthesis for probabilistic systems

10. Hybrid systems reachability analysis

Which SAT modulo theories exist? [7]

1. Quantifier-free equality logic with uninterpreted functions

2. Quantifier-free bit-vector arithmetic

3. Quantifier-free array theory

4. Quantifier-free integer/rational difference logic

5. (Quantifier-free) real/integer linear arithmetic

6. (Quantifier-free) real/integer non-linear arithmetic

7. Combined theories