TY  - INPR
A1  - Arnold, Holger
T1  - A linearized DPLL calculus with clause learning (2nd, revised version)
N2  - Many formal descriptions of DPLL-based SAT algorithms either do not include all essential proof techniques applied by modern SAT solvers or are bound to particular heuristics or data structures. This makes it difficult to analyze proof-theoretic properties or the search complexity of these algorithms. In this paper we try to improve this situation by developing a nondeterministic proof calculus that models the functioning of SAT algorithms based on the DPLL calculus with clause learning. This calculus is independent of implementation details yet precise enough to enable a formal analysis of realistic DPLL-based SAT algorithms.
N2  - Viele formale Beschreibungen DPLL-basierter SAT-Algorithmen enthalten entweder nicht alle wesentlichen Beweistechniken, die in modernen SAT-Solvern implementiert sind, oder sind an bestimmte Heuristiken oder Datenstrukturen gebunden. Dies erschwert die Analyse beweistheoretischer Eigenschaften oder der Suchkomplexität derartiger Algorithmen. Mit diesem Artikel versuchen wir, diese Situation durch die Entwicklung eines nichtdeterministischen Beweiskalküls zu verbessern, der die Arbeitsweise von auf dem DPLL-Kalkül basierenden SAT-Algorithmen mit Klausellernen modelliert. Dieser Kalkül ist unabhängig von Implementierungsdetails, aber dennoch präzise genug, um eine formale Analyse realistischer DPLL-basierter SAT-Algorithmen zu ermöglichen.
KW  - Automatisches Beweisen
KW  - Logikkalkül
KW  - SAT
KW  - DPLL
KW  - Klausellernen
KW  - automated theorem proving
KW  - logical calculus
KW  - SAT
KW  - DPLL
KW  - clause learning
Y1  - 2009
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-29080
ER  - 
TY  - INPR
A1  - Margaria, Tiziana
A1  - Hinchey, Mike
T1  - Simplicity in IT - the power of less
T2  - Computer : innovative technology for computer professionals
N2  - Simplicity is a mindset, a way of looking at solutions, an extremely wide-ranging philosophical stance on the world, and thus a deeply rooted cultural paradigm. The culture of "less" can be profoundly disruptive, cutting out existing "standard" elements from products and business models, thereby revolutionizing entire markets.
Y1  - 2013
U6  - https://doi.org/10.1109/MC.2013.397
SN  - 0018-9162
SN  - 1558-0814
VL  - 46
IS  - 11
SP  - 23
EP  - 25
PB  - Inst. of Electr. and Electronics Engineers
CY  - Los Alamitos
ER  - 
TY  - INPR
A1  - Lucke, Ulrike
A1  - Steinmetz, Ralf
T1  - Special issue on "Pervasive Education"
T2  - Pervasive and mobile computing
Y1  - 2014
U6  - https://doi.org/10.1016/j.pmcj.2014.08.001
SN  - 1574-1192
SN  - 1873-1589
VL  - 14
SP  - 1
EP  - 2
PB  - Elsevier
CY  - Amsterdam
ER  - 
TY  - INPR
A1  - Kröning, Daniel
A1  - Margaria, Tiziana
A1  - Woodcock, Jim
T1  - Untitled
T2  - Formal aspects of computing : the international journal of formal methods
Y1  - 2011
U6  - https://doi.org/10.1007/s00165-011-0201-8
SN  - 0934-5043
VL  - 23
IS  - 5
SP  - 585
EP  - 588
PB  - Springer
CY  - New York
ER  - 
TY  - INPR
A1  - Rosamond, Frances
A1  - Bardohl, Roswitha
A1  - Diehl, Stephan
A1  - Geisler, Uwe
A1  - Bolduan, Gordon
A1  - Lessmoellmann, Annette
A1  - Schwill, Andreas
A1  - Stege, Ulrike
T1  - Virtual extension reaching out to the media  become a computer science ambassador
T2  - Communications of the ACM / Association for Computing Machinery
Y1  - 2011
U6  - https://doi.org/10.1145/1897852.1897880
SN  - 0001-0782
VL  - 54
IS  - 3
SP  - 113
EP  - 116
PB  - Association for Computing Machinery
CY  - New York
ER  -