Boolean:	`(bicycle AND helmet) OR (head AND protection)` (always group AND in parenthesis)
Title:	`title:(climate change)`
Author:	`author:("bohr niels" OR "bohr n")` (avoid only full first name)
Phrase:	`"water pump control"` (does not work with wildcards)
Wildcards:	`wom?n pharm*`

Conference paper

Code Generation for a Simple First-Order Prover

In Proceedings of the Isabelle Workshop 2016 — 2016

By Villadsen, Jørgen^1,2; Schlichtkrull, Anders^1,2; From, Andreas Halkjær^1,2

From

Department of Applied Mathematics and Computer Science, Technical University of Denmark¹

Algorithms and Logic, Department of Applied Mathematics and Computer Science, Technical University of Denmark²

Abstract

We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.

Language:	English
Year:	2016
Proceedings:	Isabelle Workshop 2016
Types:	Conference paper
ORCIDs:	Villadsen, Jørgen , Schlichtkrull, Anders and From, Andreas Halkjær

Keywords

Code generation Completeness First-order logic Isabelle/HOL Isabelle/ML Soundness Standard ML Unfolding rules

Code Generation for a Simple First-Order Prover

DTU Library

Address

Shortcuts

Log in?

Code Generation for a Simple First-Order Prover

DTU Library

Address

Shortcuts