Institut für Informatik und Computational Science
Refine
Year of publication
- 2007 (36) (remove)
Document Type
- Article (23)
- Monograph/Edited Volume (6)
- Doctoral Thesis (5)
- Master's Thesis (1)
- Other (1)
Language
- English (36) (remove)
Keywords
- 3D Linsen (1)
- 3D lenses (1)
- Antwortmengenprogrammierung (1)
- Automated Theorem Proving (1)
- Automatisches Beweisen (1)
- Bilddatenanalyse (1)
- Clause Learning (1)
- DPLL (1)
- Echtzeitanwendung (1)
- Geometrieerzeugung (1)
- I/O-effiziente Algorithmen (1)
- Klausellernen (1)
- Künstliche Intelligenz (1)
- Präferenzen (1)
- SAT (1)
- Segmentierung (1)
- Shader (1)
- Skelettberechnung (1)
- Virtuelles 3D Stadtmodell (1)
- Visualisierung (1)
- answer set programming (1)
- artificial intelligence (1)
- bild (1)
- external memory algorithms (1)
- geometry generation (1)
- image (1)
- image data analysis (1)
- logic programming (1)
- logische Programmierung (1)
- medical (1)
- medizinisch (1)
- preferences (1)
- priorities (1)
- real-time application (1)
- segmentation (1)
- shader (1)
- skeletonization (1)
- virtual 3D city model (1)
- visualization (1)
Institute
This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus.