Search

Your search keyword '"Van Gelder, Allen"' showing total 235 results
Start Over Author "Van Gelder, Allen"
235 results on '"Van Gelder, Allen"'

1. Partial Boolean Functions for QBF Semantics

Author

van Gelder, Allen, Hartmanis, Juris, Founding Editor, Goos, Gerhard, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Barneva, Reneta P., editor, Brimkov, Valentin E., editor, Gentile, Claudio, editor, and Pacchiano, Aldo, editor

Published
2024
Full Text
View/download PDF

2. Subsumption-Linear Q-Resolution for QBF Theorem Proving

Author

Van Gelder, Allen, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Hansen, Helle Hvid, editor, Scedrov, Andre, editor, and de Queiroz, Ruy J.G.B., editor

Published
2023
Full Text
View/download PDF

3. The QBF Gallery: Behind the Scenes

Author

Lonsing, Florian, Seidl, Martina, and Van Gelder, Allen

Subjects
Computer Science - Logic in Computer Science
Abstract

Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks., Comment: preprint of an article to appear in Artificial Intelligence, Elsevier, 2016

Published
2015
Full Text
View/download PDF

4. Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation

Author

Lonsing, Florian, Egly, Uwe, Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Järvisalo, Matti, editor, and Van Gelder, Allen, editor

Published
2013
Full Text
View/download PDF

5. Primal and Dual Encoding from Applications into Quantified Boolean Formulas

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Schulte, Christian, editor

Published
2013
Full Text
View/download PDF

6. Contributions to the Theory of Practical Quantified Boolean Formula Solving

Author

Van Gelder, Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Milano, Michela, editor

Published
2012
Full Text
View/download PDF

7. Extended Failed-Literal Preprocessing for Quantified Boolean Formulas

Author

Van Gelder, Allen, Wood, Samuel B., Lonsing, Florian, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cimatti, Alessandro, editor, and Sebastiani, Roberto, editor

Published
2012
Full Text
View/download PDF

8. Variable Independence and Resolution Paths for Quantified Boolean Formulas

Author

Van Gelder, Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Lee, Jimmy, editor

Published
2011
Full Text
View/download PDF

9. Generalized Conflict-Clause Strengthening for Satisfiability Solvers

Author

Van Gelder, Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Sakallah, Karem A., editor, and Simon, Laurent, editor

Published
2011
Full Text
View/download PDF

10. Careful Ranking of Multiple Solvers with Timeouts and Ties

Author

Van Gelder, Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Sakallah, Karem A., editor, and Simon, Laurent, editor

Published
2011
Full Text
View/download PDF

11. Zero-One Designs Produce Small Hard SAT Instances

Author

Van Gelder, Allen, Spence, Ivor, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Strichman, Ofer, editor, and Szeider, Stefan, editor

Published
2010
Full Text
View/download PDF

12. Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces

Author

Van Gelder, Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Kullmann, Oliver, editor

Published
2009
Full Text
View/download PDF

13. Verifying Propositional Unsatisfiability: Pitfalls to Avoid

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Rangan, C. Pandu, editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Marques-Silva, João, editor, and Sakallah, Karem A., editor

Published
2007
Full Text
View/download PDF

14. Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Biere, Armin, editor, and Gomes, Carla P., editor

Published
2006
Full Text
View/download PDF

15. Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation

Author

Van Gelder, Allen, Sutcliffe, Geoff, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Furbach, Ulrich, editor, and Shankar, Natarajan, editor

Published
2006
Full Text
View/download PDF

16. Using the TPTP Language for Writing Derivations and Finite Interpretations

Author

Sutcliffe, Geoff, Schulz, Stephan, Claessen, Koen, Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Furbach, Ulrich, editor, and Shankar, Natarajan, editor

Published
2006
Full Text
View/download PDF

17. Input Distance and Lower Bounds for Propositional Resolution Proof Length

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Bacchus, Fahiem, editor, and Walsh, Toby, editor

Published
2005
Full Text
View/download PDF

18. Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Sutcliffe, Geoff, editor, and Voronkov, Andrei, editor

Published
2005
Full Text
View/download PDF

43. Independently Checkable Proofs from Decision Procedures: Issues and Progress

Author

Van Gelder, Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Sutcliffe, Geoff, editor, and Voronkov, Andrei, editor

Published
2005
Full Text
View/download PDF

47. The well-founded semantics for general logic programs

Author

Van Gelder, Allen, Ross, Kenneth A., and Schlipf, John S.

Subjects
Mathematical Logic, Formal Languages, Programming Language, Program Logic, Theorem Proving, Artificial Intelligence, Deductive Reasoning, Semantics
Published
1991

48. Direct Volume Rendering with Shading via Three-Dimensional Textures

Author

Van Gelder, Allen and Kim, Kwansik

Subjects
Computer Programming And Software
Abstract

A new and easy-to-implement method for direct volume rendering that uses 3D texture maps for acceleration, and incorporates directional lighting, is described. The implementation, called Voltx, produces high-quality images at nearly interactive speeds on workstations with hardware support for three-dimensional texture maps. Previously reported methods did not incorporate a light model, and did not address issues of multiple texture maps for large volumes. Our research shows that these extensions impact performance by about a factor of ten. Voltx supports orthographic, perspective, and stereo views. This paper describes the theory and implementation of this technique, and compares it to the shear-warp factorization approach. A rectilinear data set is converted into a three-dimensional texture map containing color and opacity information. Quantized normal vectors and a lookup table provide efficiency. A new tesselation of the sphere is described, which serves as the basis for normal-vector quantization. A new gradient-based shading criterion is described, in which the gradient magnitude is interpreted in the context of the field-data value and the material classification parameters, and not in isolation. In the rendering phase, the texture map is applied to a stack of parallel planes, which effectively cut the texture into many slabs. The slabs are composited to form an image.

Published
1996

Catalog

Books, media, physical & digital resources
See catalog results