Lecture

Second Order Logic: WS1S and HOL

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.

Description

This lecture covers the concepts of Second Order Logic (SOL), Weak Monadic Second Order Logic, and Weak Monadic Second Order Logic of 1 Successor. It explains the syntax and semantics of WS1S formulas, decision procedures, atomic and composite formulas, and the embedding function translating WS1S formulae into HOL formulae. The lecture also discusses the combination of WS1S and MONA with HOL and Isabelle, illustrating how to express problems in HOL and automatically solve subproblems in WS1S. The presentation concludes with the oracle usage, correctness, and theorems related to WS1S and HOL.

Official source

Related concepts (27)

Atomic formula

In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic. Compound formulas are formed by combining the atomic formulas using the logical connectives.

Well-formed formula

In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can be identified with the set of formulas in the language. A formula is a syntactic object that can be given a semantic meaning by means of an interpretation. Two key uses of formulas are in propositional logic and predicate logic.

Second-order logic

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).

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.

Semantics

Semantics () is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and computer science. In English, the study of meaning in language has been known by many names that involve the Ancient Greek word σῆμα (sema, "sign, mark, token"). In 1690, a Greek rendering of the term semiotics, the interpretation of signs and symbols, finds an early allusion in John Locke's An Essay Concerning Human Understanding: The third Branch may be called σημειωτική [simeiotikí, "semiotics"], or the Doctrine of Signs, the most usual whereof being words, it is aptly enough termed also λογικὴ, Logick.

Related lectures (40)

Big-step semantics: Defining arithmetic expressions and commands

Covers the definition of a simple programming language and its big-step semantics, including arithmetic expressions and imperative commands.

Semantics in Computer Language Processing: Understanding Meaning

Covers the semantics of programming languages, focusing on the Add language and the role of rewriting rules and CK machines in understanding meaning.

Type Rules: Progress and Preservation

Covers Amyli, a tiny functional language, type rules, and soundness.

Automating First-Order Logic Proofs Using Resolution

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

Polymorphism in Coq: Data Structures and Functions