آموزش منطق برای علوم کامپیوتر - آخرین آپدیت

منطق گزاره‌ای Propositional Logic

• معرفی منطق Introducing Logic

• مقدمه‌ای بر منطق گزاره‌ای Introduction to Propositional Logic

• نیاز به منطق صوری در علوم کامپیوتر Need for Formal Logics in Computer Science

• ابهام در زبان طبیعی: یک مثال Ambiguity of Natural Language: An Example

• منطق گزاره‌ای: تمایز بین نحو و معناشناسی Propositional Logic: The Distinction Between Syntax and Semantics

• جملات اخباری: یک مثال Declarative Sentences: An Example

• مقدمه‌ای بر رابط‌ها در منطق گزاره‌ای و معانی غیررسمی آن‌ها Introduction to Connectives in Propositional Logic and Their Informal Meanings

• نحو منطق گزاره‌ای Propositional Logic Syntax

• مثال‌هایی از فرمول‌های خوش‌ساخت Examples of a Well-Formed Formula

• جمع‌بندی: منطق گزاره‌ای Summary: Propositional Logic

استنتاج طبیعی در منطق گزاره‌ای Natural Deduction in Propositional Logic

• استنتاج طبیعی در منطق گزاره‌ای Natural Deduction in Propositional Logic

• سیستم‌های اثبات: نمادگذاری‌ها Proof Systems: Notations

• استنتاج طبیعی: قانون عطف Natural Deduction: Conjunction Rule

• استنتاج طبیعی: قوانین عطف - یک مثال ابتدایی Natural Deduction: Conjunction Rules—An Elementary Example

• استنتاج طبیعی: قانون استلزام Natural Deduction: Implication Rule

• استنتاج طبیعی: قوانین نفی Natural Deduction: Negation Rules

• استنتاج طبیعی: قوانین فصل Natural Deduction: Disjunction Rules

• مثال ۱: مودوس تولنز Example 1: Modus Tollens

• مثال ۲: اثبات به روش تناقض Example 2: Proof by Contradiction

• مثال ۳: قانون طرد شق ثالث Example 3: Law of Excluded Middle

• مثال ۴: اثبات استنتاج طبیعی برای یک هم‌ارزی منطقی Example 4: Natural Deduction Proof of a Logical Identity

• جمع‌بندی: استنتاج طبیعی در منطق گزاره‌ای Summary: Natural Deduction in Propositional Logic

معناشناسی، صحت و کامل بودن استنتاج طبیعی Semantics, Soundness, and Completeness of Natural Deduction

• معناشناسی، صحت و کامل بودن استنتاج طبیعی Semantics, Soundness, and Completeness of Natural Deduction

• تفسیر فرمول‌های منطق گزاره‌ای Interpretation of Propositional Logic Formulas

• تفسیر یک فرمول پیچیده: روش جدول حقیقت Interpretation of a Complex Formula: The Truth Table Method

• توتولوژی‌ها و مغالطه‌ها، قابلیت ارضا و اعتبار Tautologies and Fallacies, Satisfiability, and Validity

• بررسی قابلیت ارضا با استفاده از روش جدول حقیقت Satisfiability Using Truth Table Method

• هم‌ارزی معنایی و مجموعه کافی از رابط‌ها Semantic Equivalence, and Adequate Set of Connectives

• فرم‌های نرمال: CNF و DNF Normal Forms: CNF and DNF

• قابلیت ارضا و اعتبار: دوگانگی Satisfiability and Validity: Duality

• اثبات قابلیت ارضا با استفاده از روش رزولوشن Satisfiability Proof Using Resolution

• الگوریتم دیویس-پاتنام: مقدمه Davis Putnam Algorithm: An Introduction

• الگوریتم دیویس-پاتنام: یک مثال عملی Davis Putnam Algorithm: A Running Example

• توسعه تئوری منطقی: نگاهی دوباره به استنتاج طبیعی Development of Logical Theory: A Look Back at Natural Deduction

• صحت و کامل بودن استنتاج طبیعی Soundness and Completeness of Natural Deduction

• جمع‌بندی: معناشناسی، صحت و کامل بودن استنتاج طبیعی Summary: Semantics, Soundness, and Completeness of Natural Deduction

تکنیک‌های بررسی مدل و منطق‌های زمانی Model Checking Techniques and Temporal Logics

• تکنیک‌های بررسی مدل و منطق‌های زمانی Model Checking Techniques and Temporal Logics

• رویکردهای تایید کامپیوتری Approaches to Computer Verification

• بررسی مدل (Model Checking) Model Checking

• سیستم انتقال: یک مثال Transition System: An Example

• تعریف صوری: سیستم انتقال Formal Definition: Transition System

• مسیرها و ردپاها: یک مثال Paths and Traces: An Example

• ناورداها، ویژگی‌های ایمنی و زنده بودن Invariants, Safety, and Liveness Properties

• مثال‌هایی از ویژگی‌های LTI Examples of LTI Properties

• مرور مجدد: مراحل بررسی مدل Revisiting: Model Checking Steps

• خانواده منطق‌های زمانی Family of Temporal Logics

• منطق زمانی خطی (LTL): مقدمه‌ای غیررسمی Linear Temporal Logic: An Informal Introduction

• منطق درخت محاسباتی (CTL): مقدمه‌ای غیررسمی Computation Tree Logic: An Informal Introduction

• جمع‌بندی: تکنیک‌های بررسی مدل و منطق‌های زمانی Summary: Model Checking Techniques and Temporal Logics

منطق‌های زمانی LTL و CTL و الگوریتم‌های بررسی مدل LTL and CTL Temporal Logics, Algorithms for Model Checking

• بررسی مدل Model Checking

• نحو LTL LTL Syntax

• مثال‌ها: تبدیل جملات زبان طبیعی به LTL Examples: Encoding of Natural Language Sentence into LTL

• معناشناسی LTL LTL Semantics

• هم‌ارزی‌های فرمول LTL Equivalences of LTL Formula

• عملگرهای Release و Weak Until Release and Weak Until Operators

• بررسی مدل LTL: ایده ساده LTL Model Checking: Naive Idea

• بررسی مدل LTL: بحث در مورد ویژگی‌های غیرقابل بیان در LTL LTL Model Checking : Discussion on Properties Inexpressible in LTL

• منطق درخت محاسباتی: نحو Computational Tree Logic: The Syntax

• مثال‌ها: تبدیل جملات زبان طبیعی به CTL Examples: Encoding of Natural Language Sentence into CTL

• منطق درخت محاسباتی: معناشناسی Computational Tree Logic: The Semantics

• الگوریتم بررسی مدل برای CTL: ایده ساده Model Checking Algorithm for CTL: Naive Idea

• جمع‌بندی: منطق‌های زمانی و الگوریتم‌های بررسی مدل Summary: Temporal Logics and Algorithms for Model Checking

منطق محمولاتی Predicate Logic

• منطق محمولاتی Predicate Logic

• نیاز به منطق محمولاتی Need for Predicate Logic

• قدرت بیان محمولات: متغیرها و کوانتیفایه‌ها - بخش اول Expressiveness of Predicates: Variables and Quantifiers—Part I

• قدرت بیان محمولات: متغیرها و کوانتیفایه‌ها - بخش دوم Expressiveness of Predicates: Variables and Quantifiers—Part II

• قدرت بیان محمولات: آرگومان‌های محمولات Expressiveness of Predicates: Arguments of Predicates

• قدرت بیان محمولات: عبارت‌های تابعی Expressiveness of Predicates: Function Terms

• قدرت بیان محمولات: روابط غیرقطعی Expressiveness of Predicates: Non-deterministic Relations

• بیان با استفاده از محمولات: قراردادها و مثال‌های ۱ Expressing Using Predicates: Conventions and Examples 1

• بیان با استفاده از محمولات: قراردادها و مثال‌های ۲ Expressing Using Predicates: Conventions and Examples 2

• بیان با استفاده از محمولات: مثال‌های ۳ Expressing Using Predicates: Examples 3

• بیان با استفاده از محمولات: مثال‌های ۴ Expressing Using Predicates: Examples 4

• بیان با استفاده از محمولات: مثال ۵ Expressing Using Predicates: Example 5

• بیان با استفاده از محمولات: مثال‌های ۶ Expressing Using Predicates: Examples 6

• بیان قوانین استقرایی با استفاده از منطق محمولاتی Expressing Inductive Rules Using Predicate Logic

• نحو منطق محمولاتی Syntax of Predicate Logic

• منطق محمولاتی: قراردادهای مورد استفاده Predicate Logic: Conventions Used

• حذف کوانتیفایر کلی با مثال‌ها Universal Quantifier Elimination with Examples

• معرفی کوانتیفایر وجودی با مثال‌ها Existential Quantifier Introduction with Examples

• جایگزینی و اتصال Substitution and Binding

• متغیرهای متصل در مقابل متغیرهای آزاد Bound vs. Free Variables

• مرور مجدد جایگزینی Substitution Revisited

• جایگزینی و تغییر نام Substitution and Renaming

• جمع‌بندی: منطق محمولاتی Summary: Predicate Logic

استنتاج طبیعی در منطق محمولاتی Natural Deduction in Predicate Logic

• استنتاج طبیعی در منطق محمولاتی Natural Deduction in Predicate Logic

• قوانین اثبات برای استنتاج طبیعی در منطق گزاره‌ای: مرور Proof Rules for Natural Deduction in Propositional Logic: Revision

• حذف کوانتیفایر کلی و معرفی کوانتیفایر وجودی: مثال‌ها Universal Quantifier Elimination and Existential Quantifier Introduction: Examples

• معرفی کوانتیفایر کلی با مثال Universal Quantifier Introduction with Example

• حذف کوانتیفایر وجودی با مثال Existential Quantifier Elimination with Example

• معرفی کوانتیفایر کلی در مقابل حذف کوانتیفایر وجودی Universal Quantifier Introduction vs. Existential Quantifier Elimination

• استنتاج طبیعی در منطق محمولاتی: مثال ۱ ND in Predicate Logic: Example 1

• استنتاج طبیعی در منطق محمولاتی: مثال ۲ ND in Predicate Logic: Example 2

• استنتاج طبیعی در منطق محمولاتی: مثال ۳ ND in Predicate Logic: Example 3

• استنتاج طبیعی در منطق محمولاتی: مثال ۴ ND in Predicate Logic: Example 4

• استنتاج طبیعی در منطق محمولاتی: مثال ۵ ND in Predicate Logic: Example 5

• استنتاج طبیعی در منطق محمولاتی: مثال ۶ ND in Predicate Logic: Example 6

• استنتاج طبیعی در منطق محمولاتی: مثال ۷ ND in Predicate Logic: Example 7

• استنتاج طبیعی در منطق محمولاتی: مثال ۸ ND in Predicate Logic: Example 8

• استنتاج طبیعی در منطق محمولاتی: مثال ۹ ND in Predicate Logic: Example 9

• استنتاج طبیعی در منطق محمولاتی: مثال ۱۰ ND in Predicate Logic: Example 10

• جمع‌بندی: استنتاج طبیعی در منطق محمولاتی Summary: Natural Deduction in Predicate Logic

معناشناسی، صحت، کامل بودن و تصمیم‌ناپذیری منطق محمولاتی Semantics, Soundness, Completeness, and Undecidability of Predicate Logic

• معرفی بخش: معناشناسی، صحت، کامل بودن و تصمیم‌ناپذیری منطق محمولاتی Module Introduction: Semantics, Soundness, Completeness, and Undecidability of Predicate Logic

• معناشناسی در منطق محمولاتی: مقدمه - بخش اول Semantics in Predicate Logic: Introduction—Part I

• معناشناسی در منطق محمولاتی: مقدمه - بخش دوم Semantics in Predicate Logic: Introduction—Part II

• معناشناسی: مدل‌ها و تفسیرها - بخش ۱ Semantics: Models and Interpretations—Part 1

• معناشناسی: مدل‌ها و تفسیرها - بخش ۲ Semantics: Models and Interpretations—Part 2

• معناشناسی: مدل‌ها و تفسیرها - بخش ۳ Semantics: Models and Interpretations—Part 3

• معناشناسی: مدل‌ها و تفسیرها - بخش ۴ Semantics: Models and Interpretations—Part 4

• معناشناسی: مدل‌ها و تفسیرها - بخش ۵ Semantics: Models and Interpretations—Part 5

• معناشناسی: تفسیر شامل متغیرها Semantics: Interpretation Involving Variables

• معناشناسی: تفسیر با استفاده از محیط‌ها یا جداول جستجو Semantics: Interpretation Using Environments or Look-Up Tables

• بررسی رابطه مدل با مثال‌ها Model Checks Relation with Examples

• استلزام معنایی Semantic Entailment

• قابلیت ارضا و اعتبار در منطق محمولاتی Satisfiability and Validity in Predicate Logic

• قابلیت ارضا و اعتبار: مثال ۱ Satisfiability and Validity: Example 1

• قابلیت ارضا و اعتبار: مثال ۲ Satisfiability and Validity: Example 2

• قابلیت ارضا و اعتبار: مثال ۳ Satisfiability and Validity: Example 3

• قابلیت ارضا و اعتبار: مثال ۴ Satisfiability and Validity: Example 4

• تصمیم‌ناپذیری، صحت و کامل بودن منطق محمولاتی Undecidability, Soundness, and Completeness of Predicate Logic

• محدودیت‌های منطق مرتبه اول و نگاهی به منطق مرتبه دوم Limitations of First-Order Logic and a Glimpse of Second-Order Logic

• جمع‌بندی: معناشناسی، صحت، کامل بودن و تصمیم‌ناپذیری منطق محمولاتی Summary: Semantics, Soundness, Completeness, and Undecidability of Predicate Logic

تایید برنامه‌ها Program Verification

• معرفی بخش: تایید برنامه‌ها Module Introduction: Program Verification

• تایید صوری: انگیزه Formal Verification: Motivation

• منطق فلوید-هوآر: مقدمه، صحت جزئی در مقابل صحت کلی Floyd-Hoare Logic: Introduction, and Partial vs. Total Correctness

• منطق فلوید-هوآر: صحت دستورات تخصیص Floyd-Hoare Logic: Correctness of Assignment Statements

• منطق فلوید-هوآر: صحت توالی Floyd-Hoare Logic: Correctness of Sequencing

• منطق فلوید-هوآر: کاربردهای عملی Floyd-Hoare Logic: Pragmatics

• منطق فلوید-هوآر: صحت دستورات شرطی Floyd-Hoare Logic: Correctness of Conditionals

• منطق فلوید-هوآر: متارول و مثال‌ها Floyd-Hoare Logic: Meta-Rule and Examples

• استدلال‌های پایان‌پذیری برای صحت کلی Termination Arguments for Total Correctness

• مثال‌های استدلال پایان‌پذیری ۱ Termination Arguments Examples 1

• مثال‌های استدلال پایان‌پذیری ۲ Termination Arguments Examples 2

• متغیرهای برنامه در مقابل متغیرهای منطقی Program Variables vs. Logical Variables

• تایید صحت حلقه‌ها: ناوردای حلقه با مثال‌ها Verifying Correctness of Loops: Loop Invariants with Examples

• ناوردای حلقه: مثال ۱ Loop Invariants: Example 1

• ناوردای حلقه: مثال ۲ Loop Invariants: Example 2

• جمع‌بندی: تایید برنامه‌ها Summary: Program Verification

مطالعات موردی تایید برنامه‌ها Program Verification Case Studies

• معرفی بخش: تایید برنامه‌ها: مطالعات موردی Module Introduction: Program Verification: Case Studies

• محاسبه توان دو عدد: صحت جزئی  Computing Power of two numbers: Partial Correctness

• محاسبه توان دو عدد: اثبات پایان‌پذیری Computing Power of two numbers: Proof of Termination

• یافتن یک عنصر در یک آرایه نامرتب Finding an Element in an Unsorted Array

• یافتن یک عنصر در یک آرایه نامرتب: صحت کلی Finding an Element in an Unsorted Array: Total Correctness

• مرتب‌سازی انتخابی: شهود Selection Sort: Intuition

• مرتب‌سازی انتخابی: برنامه C Selection Sort: C Program

• مرتب‌سازی انتخابی: صحت تابع findMinIndex() Selection Sort: Correctness of findMinIndex()

• مرتب‌سازی انتخابی: صحت تابع sort() Selection Sort: Correctness of sort()

• جمع‌بندی: مطالعات موردی تایید برنامه‌ها Summary: Program Verification Case Studies

• جمع‌بندی نهایی دوره Course Wrap-up