Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

Extracting verified decision procedures: DPLL and Resolution

Ulrich Berger ; Andrew Lawrence ; Fredrik Nordvall Forsberg ; Monika Seisenberger.
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and&nbsp;[&hellip;]
Published on March 10, 2015
Volume 11, Issue 1

Positive Inductive-Recursive Definitions

Neil Ghani ; Fredrik Nordvall Forsberg ; Lorenzo Malatesta.
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within&nbsp;[&hellip;]
Published on March 27, 2015
Volume 11, Issue 1
  • < Previous
  • 1
  • Next >