Partenaire Premium

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
Attribution de licence Non précisé
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)