Book chapter
Lemma Learning in the Model Evolution Calculus
Logic for Programming, Artificial Intelligence, and Reasoning, pp.572-586
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2006
DOI: 10.1007/11916277_39
Abstract
The Model Evolution \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{ME}$\end{document} Calculus is a proper lifting to first-order logic of the DPLL procedure, a backtracking search procedure for propositional satisfiability. Like DPLL, the ME calculus is based on the idea of incrementally building a model of the input formula by alternating constraint propagation steps with non-deterministic decision steps. One of the major conceptual improvements over basic DPLL is lemma learning, a mechanism for generating new formulae that prevent later in the search combinations of decision steps guaranteed to lead to failure. We introduce two lemma generation methods for \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{ME}$\end{document} proof procedures, with various degrees of power, effectiveness in reducing search, and computational overhead. Even if formally correct, each of these methods presents complications that do not exist at the propositional level but need to be addressed for learning to be effective in practice for \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{ME}$\end{document}. We discuss some of these issues and present initial experimental results on the performance of an implementation of the two learning procedures within our \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{ME}$\end{document} prover Darwin.
Details
- Title: Subtitle
- Lemma Learning in the Model Evolution Calculus
- Creators
- Peter Baumgartner - Data61Alexander Fuchs - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Logic for Programming, Artificial Intelligence, and Reasoning, pp.572-586
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/11916277_39
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2006
- Academic Unit
- Computer Science
- Record Identifier
- 9984259422802771
Metrics
2 Record Views