Mercurial > 13ws.ds

comparison notes/tex/logic.tex @ 22:dc6b569c57c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fifth slides and sheet
author Markus Kaiser <markus.kaiser@in.tum.de>
date Mon, 18 Nov 2013 23:49:37 +0100
parents d9b98c2ba5ac
children 41623ba498a9
comparison
equal deleted inserted replaced
21:03a0cf37ddaa 22:dc6b569c57c8
495 \end{definition} 495 \end{definition}
496 496
497 \begin{block}{DPLL} 497 \begin{block}{DPLL}
498 Gegeben eine Formel $F$ in KNF 498 Gegeben eine Formel $F$ in KNF
499 \begin{itemize} 499 \begin{itemize}
500 \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar} 500 \item Wenn $F = \mathrm{true}$ dann antworte \structure{erfüllbar}
501 \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar} 501 \item Wenn $F = \mathrm{false}$ dann antworte \structure{unerfüllbar}
502 \item Sonst 502 \item Sonst
503 \begin{enumerate} 503 \begin{enumerate}
504 \item Wähle eine Variable $p$ in $F$ 504 \item Wähle eine Variable $p$ in $F$
505 \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar 505 \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar
506 \end{enumerate} 506 \end{enumerate}
510 \item Schlaue Wahl der Variable beschleunigt Ausführung 510 \item Schlaue Wahl der Variable beschleunigt Ausführung
511 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) 511 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule})
512 \end{itemize} 512 \end{itemize}
513 \end{frame} 513 \end{frame}
514 } 514 }
515
516 \defineUnit{resolution}{%
517 \begin{frame}
518 \frametitle{Resolution}
519 \setbeamercovered{dynamic}
520
521 \begin{definition}[Resolvent]
522 Seien $K_1$, $K_2$ und $R$ Klauseln in Mengendarstellung. Dann heißt $R$ \structure{Resolvent} von $K_1$ und $K_2$ wenn $L \in K_1$, $\neg L \in K_2$ und
523 \begin{align}
524 R &= \left( K_1 \setminus \left\{ L \right\} \right) \cup \left( K_2 \setminus \left\{ \neg L \right\} \right)
525 \end{align}
526 \end{definition}
527
528 \begin{block}{Resolution}
529 Gegeben eine Formel $F$ in KNF in Mengendarstellung.
530 \begin{algorithmic}
531 \While{$\square = \emptyset \not \in F$}
532 \State{$R \gets \text{Resolvent aus } F \text{ mit } R \not\in F$}
533 \If{$R$ existiert}
534 \State{$F \gets F \cup R$}
535 \Else
536 \State{\textbf{return} \structure{erfüllbar}}
537 \EndIf
538 \EndWhile
539 \State{\textbf{return} \structure{unerfüllbar}}
540 \end{algorithmic}
541 \end{block}
542 \end{frame}
543 }
544
545 \defineUnit{natuerlichesschliessen}{%
546 \begin{frame}
547 \frametitle{Kalküle}
548 \setbeamercovered{dynamic}
549
550 \begin{definition}[Kalkül]
551 Ein \structure{Logikkalkül} stellt \structure{Inferenzregeln} bereit, mit denen Formeln \alert{syntaktisch} umgeformt werden können.
552 \end{definition}
553
554 \begin{definition}[Folgerung]
555 $F$ \structure{folgt aus} $A$, wenn mit Hilfe der \alert{Semantik} der \alert{Aussagenlogik} $F$ unter der Annahme dass $A$ gilt zu $\mathrm{true}$ ausgewertet wird. Wir schreiben
556 \[ A \vDash F \]
557 \end{definition}
558
559 \begin{definition}[Ableitung]
560 $F$ kann aus $A$ \structure{abgeleitet} werden, wenn mit Hilfe \alert{syntaktischer} Umformungen in einem \alert{Logikkalkül} $F$ unter der Annahme $A$ bewiesen werden kann. Wir schreiben
561 \[ A \vdash F \]
562 \end{definition}
563 \end{frame}
564
565 \begin{frame}
566 \frametitle{Eigenschaften von Kalkülen}
567 \setbeamercovered{dynamic}
568
569 \begin{block}{Eigenschaften von Kalkülen}
570 \begin{description}[\quad vollständig (complete)]
571 \item[korrekt (sound)] Es können \alert{nur} semantisch gültige Formeln abgeleitet werden.
572 \[ \text{Aus } A \vdash F \text{ folgt } A \vDash F \]
573 \item[vollständig (complete)] \alert{Alle} semantisch gültigen Formeln können abgeleitet werden.
574 \[ \text{Aus } A \vDash F \text{ folgt } A \vdash F \]
575 \end{description}
576 \end{block}
577
578 \begin{itemize}
579 \item Für uns nur korrekte vollständige Kalküle
580 \item Beispiel für die Aussagenlogik: \structure{Natürliches Schließen}
581 \medskip
582 \item Es gibt keine solchen Kalküle für die
583 \begin{itemize}
584 \item Prädikatenlogik
585 \item Arithmetik
586 \end{itemize}
587 \item Deshalb sind nicht alle Sätze der Mathematik beweisbar
588 \end{itemize}
589 \end{frame}
590
591 {
592 \newcommand{\F}{\phi}
593 \newcommand{\G}{\psi}
594 \newcommand{\K}{\chi}
595 \newcommand{\subproof}[2]{%
596 \begin{tikzpicture}[y=.9em]
597 \path
598 (0, 0) node (a) {##1}
599 ++(0, -1) node (b) {$\vdots$}
600 ++(0, -1) node[below] (c) {##2};
601 \node[fit=(a)(b)(c), draw, inner sep=1pt] {};
602 \end{tikzpicture}%
603 }
604 \newcommand{\topproof}[1]{%
605 ##1
606 \bottomAlignProof
607 \DisplayProof
608 }
609
610 \begin{frame}
611 \frametitle{Natürliches Schließen}
612 \setbeamercovered{dynamic}
613
614 \vspace{-4pt}
615 \tabulinesep=4pt
616 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
617 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-}
618 $\wedge$ &
619 \topproof{
620 \AxiomC{$\F$}
621 \AxiomC{$\G$}
622 \RightLabel{\scriptsize $+\wedge$}
623 \BinaryInfC{$\F \wedge \G$}
624 }
625 &
626 \topproof{
627 \AxiomC{$\F \wedge \G$}
628 \RightLabel{\scriptsize $-\wedge_1$}
629 \UnaryInfC{$\F$}
630 }
631 \quad
632 \topproof{
633 \AxiomC{$\F \wedge \G$}
634 \RightLabel{\scriptsize $-\wedge_2$}
635 \UnaryInfC{$\G$}
636 }
637 \\
638 $\vee$ &
639 \topproof{
640 \AxiomC{$\F$}
641 \RightLabel{\scriptsize $+\vee_1$}
642 \UnaryInfC{$\F \vee \G$}
643 }
644 \quad
645 \topproof{
646 \AxiomC{$\G$}
647 \RightLabel{\scriptsize $+\vee_2$}
648 \UnaryInfC{$\F \vee \G$}
649 }
650 &
651 \topproof{
652 \AxiomC{$\F \vee \G$}
653 \AxiomC{\subproof{$\F$}{$\K$}}
654 \AxiomC{\subproof{$\G$}{$\K$}}
655 \RightLabel{\scriptsize $-\vee$}
656 \TrinaryInfC{$\K$}
657 }
658 \\
659 $\rightarrow$ &
660 \topproof{
661 \AxiomC{\subproof{$\F$}{$\G$}}
662 \RightLabel{\scriptsize $+\rightarrow$}
663 \UnaryInfC{$\F \rightarrow \G$}
664 }
665 &
666 \topproof{
667 \AxiomC{$\F$}
668 \AxiomC{$\F \rightarrow \G$}
669 \RightLabel{\scriptsize $-\rightarrow$, MP}
670 \BinaryInfC{$\G$}
671 }
672 \\
673 $\neg$ &
674 \topproof{
675 \AxiomC{\subproof{$\F$}{$\bot$}}
676 \RightLabel{\scriptsize $+\neg$}
677 \UnaryInfC{$\neg \F$}
678 }
679 &
680 \topproof{
681 \AxiomC{$\F$}
682 \AxiomC{$\neg\F$}
683 \RightLabel{\scriptsize $-\neg$}
684 \UnaryInfC{$\bot$}
685 }
686 \end{tabu}
687 \end{frame}
688
689 \begin{frame}
690 \frametitle{Natürliches Schließen}
691 \setbeamercovered{dynamic}
692
693 \vspace{-4pt}
694 \tabulinesep=4pt
695 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
696 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-}
697 $\bot$ &
698 &
699 \topproof{
700 \AxiomC{$\bot$}
701 \RightLabel{\scriptsize $-\bot$}
702 \UnaryInfC{$\F$}
703 }
704 \\
705 $\neg\neg$ &
706 \topproof{
707 \AxiomC{$\F$}
708 \RightLabel{\scriptsize $+\neg\neg$}
709 \UnaryInfC{$\neg\neg\F$}
710 }
711 &
712 \topproof{
713 \AxiomC{$\neg\neg\F$}
714 \RightLabel{\scriptsize $-\neg\neg$}
715 \UnaryInfC{$\F$}
716 }
717 \end{tabu}
718 \begin{itemize}
719 \vfill
720 \item Praktische abgeleitete Regeln
721 \end{itemize}
722 \tabulinesep=10pt
723 \begin{tabu} to \textwidth {X[c,m,.5]X[c,b,5]X[c,b,5]}
724 &
725 \topproof{
726 \AxiomC{ }
727 \RightLabel{\scriptsize LEM}
728 \UnaryInfC{$\F \vee \neg\F$}
729 }
730 &
731 \topproof{
732 \AxiomC{\subproof{$\neg\F$}{$\bot$}}
733 \RightLabel{\scriptsize $-\neg$, PBC}
734 \UnaryInfC{$\F$}
735 }
736 \\
737 &
738 &
739 \topproof{
740 \AxiomC{$\neg\G$}
741 \AxiomC{$\F \rightarrow \G$}
742 \RightLabel{\scriptsize MT}
743 \BinaryInfC{$\neg\F$}
744 }
745 \end{tabu}
746 \end{frame}
747 }
748 }