Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Term Models for First-Order Logic

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 covers term models for first-order logic, discussing the interpretation that makes a formula true, substructures, small model theorems, examples of substructures, universal formulas staying true in substructures, finding the smallest substructure, and the Herbrand model as a generic countable model.

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 (27)

First-order logic

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.

Automated theorem proving

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science. While the roots of formalised logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics.

Resolution (logic)

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

Model theory

In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the statements of the theory hold). The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself.

Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics. The most commonly studied formal logics are propositional logic, predicate logic and their modal analogs, and for these there are standard ways of presenting an interpretation.

Related lectures (28)

Coq: Introduction

Introduces Coq, covering defining propositions, proving theorems, and using tactics.

Automating First-Order Logic Proofs Using Resolution

Covers first-order logic syntax, semantics, and resolution for proving properties.

Automating First-Order Logic Proofs Using Resolution

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

Predicate Logic: Basics and Applications

Covers the basics and applications of predicate logic, including quantifiers, predicates, and propositional functions.

Automating First-Order Logic Proofs Using Resolution

Covers first-order logic, resolution proofs, Skolem functions, and satisfiability checking in mathematics and program verification.

Related concepts (27)

First-order logic

Automated theorem proving

Resolution (logic)

Model theory

Interpretation (logic)