Lecture

Case Analysis Rule and Propositional Resolution

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

In course

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

Description

This lecture introduces a proof system for propositional formulas with decision and simplification, focusing on the case analysis rule and propositional resolution. The instructor explains the soundness of the proof system and demonstrates example derivations. The lecture covers simplification rules, unsatisfiability proofs, soundness consequences, refutation completeness, and resolution on clauses as a proof system. It also discusses conjunctive form, literals, clauses, and resolution as transitivity of implication. Exercises on using resolution to prove formula validity and unsatisfiability are included, along with unit resolution concepts.

Instructor

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Official source

Related concepts (32)

Satisfiability

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

Boolean satisfiability problem

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable.

Proof calculus

In mathematical logic, a proof calculus or a proof system is built to prove statements. A proof system includes the components: Language: The set L of formulas admitted by the system, for example, propositional logic or first-order logic. Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems. Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms. Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined and can be used for radically different logics.

Completeness (logic)

In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete. The term "complete" is also used without qualification, with differing meanings depending on the context, mostly referring to the property of semantical validity. Intuitively, a system is called complete in this particular sense, if it can derive every formula that is true.

Horn-satisfiability

In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn. A Horn clause is a clause with at most one positive literal, called the head of the clause, and any number of negative literals, forming the body of the clause. A Horn formula is a propositional formula formed by conjunction of Horn clauses. The problem of Horn satisfiability is solvable in linear time.

Related lectures (60)

Automating First-Order Logic Proofs Using Resolution

Covers first-order logic syntax, semantics, Skolemization, resolution, and normal form transformations.

Propositional Resolution

Explores completeness in propositional logic, resolution on clauses, conjunctive form, unit resolution, SAT solvers, and proof generation.

Propositional Logic: Inference Rules

Covers the interpretation of propositional logic and inference rules for implication, conjunction, and double negation.

Soundness and Completeness of a Propositional Proof System

Explores the importance of soundness and completeness in a propositional proof system.

Finite Systems Expressed with Formulas