# SC Chapter 1 Introduction

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

32
0.0 (0)

Set of flashcards Details

Flashcards 32 English Computer Science University 18.02.2017 / 18.02.2017 Not defined https://card2brain.ch/box/20170218_sc_chapter_1_introduction

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)