References

[1] John Franco and Allen Van Gelder. A perspective on certain polynomial time solvable classes of satisfiability. Discrete Applied Mathematics, 125(2–3):177–214, 2003.

[2] A. Goultiaeva, , A. Van Gelder, and F. Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Proc. IJCAI, 2011. (preprint at www.cse.ucsc.edu/˜ avg/Papers/-

strategies.pdf).

[3] Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, and Allen Van Gelder. Clause learning can effectively psimulate general propositional resolution. In Twenty-Third AAAI Conference on Artificial Intelligence (AAAI-08), pages 283–290, Chicago, July 2008. AAAI.

[4] K. Morris, J. D. Ullman, and A. Van Gelder. Design overview of the Nail! system. In Third Int’l Conf. on Logic Programming, pages 554–568, 1986.

[5] A. G. Neeman, R. Brannon, B. Jeremić, A. Pang, and A. Van Gelder. Decomposition and visualization of fourthorder elastic-plastic tensors. In IEEE/EG Symposium on Volume and Point-Based Graphics, Los Angeles, August 2008. IEEE/EG.

[6] Fumiaki Okushi and Allen Van Gelder. Persistent and quasi-persistent lemmas in propositional model elimination. Annals of Mathematics and Artificial Intelligence, 40(3–4):373–402, 2004.

[7] Tai Joon Park and Allen Van Gelder. Partitioning methods for satisfiability testing on large formulas. In Proceedings 13th International Conference on Automated Deduction, volume 1104 of LNAI, pages 748–762. Springer-Verlag, July 1996.

[8] Tai Joon Park and Allen Van Gelder. Partitioning methods for satisfiability testing on large formulas. Information and Computation, 161(2), 2000. (Extended abstract, full paper appeared in CADE-13).

[9] David Peleg and Allen Van Gelder. Packet distribution on a ring. Journal of Parallel and Distributed Computing, 6(3):558–567, 1989.

[10] Kjell Post, Allen Van Gelder, and James Kerr. Deterministic parsing of languages with dynamic operators. In International Logic Programming Symposium, October 1993.

[11] Kirack Sohn and Allen Van Gelder. Termination detection in logic programs using argument sizes. In Tenth ACM Symposium on Principles of Database Systems, pages 216–226, 1991.

[12] Jeffrey D. Ullman and Allen Van Gelder. Efficient tests for top-down termination of logical rules. Journal of the ACM, 35(2):345–373, 1988. (Preprint available from second author).

[13] Jeffrey D. Ullman and Allen Van Gelder. Parallel complexity of logical query programs. Algorithmica, 3(1):5–42, 1988. (Preprint available from second author. Short version appeared in FOCS, 1986.).

[14] A. Van Gelder. Report on relaxed Jordan canonical form for computer animation and visualization. Technical report, UC Santa Cruz, Jan. 2009. (URL: http://www.cse.ucsc.edu/ ∼avg/Papers/

rjcfTR.pdf).

[15] A. Van Gelder. Careful ranking of multiple solvers with timeouts and ties. In Proc. SAT (LNCS 6695), pages 317–328. Springer, 2011.

[16] A. Van Gelder. Generalized conflict-clause strengthening for satisfiability solvers. In Proc. SAT (LNCS 6695), pages 329–342. Springer, 2011.

[17] Allen Van Gelder. A message passing framework for logical query evaluation. In 1986 ACM-SIGMOD Conf. on Management of Data, pages 155–165, 1986.

[18] Allen Van Gelder. Efficient loop detection in Prolog using the tortoise and hare technique. Journal of Logic Programming, 4(1):23–33, 1987.

[19] Allen Van Gelder. A Satisfiability Tester for Non-Clausal Propositional Calculus. Information and Computation, 79(1):1–21, October 1988.

[20] Allen Van Gelder. Negation as failure using tight derivations for general logic programs. Journal of Logic Programming, 6(1):109–133, 1989. Preliminary versions appeared in Third IEEE Symp. on Logic Programming (1986), and Foundations of Deductive Databases and Logic Programming, J. Minker, ed., Morgan Kaufmann, 1988.

[21] Allen Van Gelder. Pram processor allocation: A hidden bottleneck in sublogarithmic algorithms. IEEE Transactions on Computers, 38(2):289–292, 1989.

[22] Allen Van Gelder. Modeling simultaneous events with default reasoning and tight derivations. Journal of Logic Programming, 8(1):41–52, 1990.

[23] Allen Van Gelder. A new form of circumscription for logic programs. Technical Report UCSC-CRL-90-50, Univ. of Calif., Santa Cruz, 1990. Extended abstract in Workshop on Logic Programming and Nonmonotonic Reasoning at 1990 NACLP.

[24] Allen Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artificial Intelligence, 1(3):361–392, 1991.

[25] Allen Van Gelder. The well-founded semantics of aggregation. In ACM Symposium on Principles of Database Systems, 1992.

[26] Allen Van Gelder. The alternating fixpoint of logic programs with negation. Journal of Computer and System Sciences, 47(1):185–221, 1993.

[27] Allen Van Gelder. Foundations of aggregation in deductive databases. In Third International Conference on Deductive and Object-Oriented Databases, Phoenix, AZ, December 1993.

[28] Allen Van Gelder. Efficient computation of polygon area and polyhedron volume. In Graphics Gems V. Academic Press, Boston, Mass., 1995.

[29] Allen Van Gelder. Approximate simulation of elastic membranes by triangulated spring meshes. Journal of Graphics Tools, 3(2):21–42, 1998.

[30] Allen Van Gelder. Propositional search with k-clause introduction can be polynomially simulated by resolution. In (Electronic) Proc. 5th Int’l Symposium on Artificial Intelligence and Mathematics, 1998.

[31] Allen Van Gelder. A tutorial on the well-founded semantics. Programmirovanie, 24(1), 1998. (Russian) Translation: Programming and Computer Software (24)1, Jan. 1998.

[32] Allen Van Gelder. Autarky pruning in propositional model elimination reduces failure redundancy. Journal of Automated Reasoning, 23(2):137–193, 1999.

[33] Allen Van Gelder. Complexity analysis of propositional resolution with autarky pruning. Discrete Applied Mathematics, 96–97:195–221, 1999.

[34] Allen Van Gelder. Lemmas in propositional model search and refutation search. In Third Workshop on the Satisfiability Problem, Renesse, Netherlands, 2000.

[35] Allen Van Gelder. Combining preorder and postorder resolution in a satisfiability solver. In IEEE/ASL LICS Satisfiability Workshop, Boston, 2001.

[36] Allen Van Gelder. Stream surface generation for fluid flow solutions on curvilinear grids. In Joint EUROGRAPHICS-IEEE TCVG Symposium on Visualization (VisSym01), Ascona, Switzerland, May 2001.

[37] Allen Van Gelder. Decision procedures should be able to produce (easily) checkable proofs. In Workshop on Constraints in Formal Verification, Ithaca, NY, 2002. (in conjunction with CP02).

[38] Allen Van Gelder. Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. In Seventh Int’l Symposium on AI and Mathematics, Ft. Lauderdale, FL, 2002.

[39] Allen Van Gelder. Generalizations of watched literals for backtracking search. In Seventh Int’l Symposium on AI and Mathematics, Ft. Lauderdale, FL, 2002.

[40] Allen Van Gelder. Input distance and lower bounds for propositional resolution proof length. In Eighth International Conference on Theory and Applications of Satisfiability Testing, St. Andrews, Scotland, 2005.

[41] Allen Van Gelder. Pool resolution and its relation to regular resolution and DPLL with clause learning. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNAI 3835, pages 580–594, Montego Bay, Jamaica, 2005. Springer-Verlag.

[42] Allen Van Gelder. Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence, 43(1–4):239–253, 2005. (Preliminary version appeared in SAT02, Cincinnati).

[43] Allen Van Gelder. Preliminary report on input cover number as a metric for propositional resolution proofs. In Theory and Applications of Satisfiability Testing, (SAT), LNCS 4121, pages 48–53, Seattle, WA, 2006.

[44] Allen Van Gelder. Verifying propositional unsatisfiability: Pitfalls to avoid. In Tenth International Conference on Theory and Applications of Satisfiability Testing, Lisboa, Portugal, 2007.

[45] Allen Van Gelder. Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics, 156(2):230–243, January 2008. (Preliminary version appeared in COLOR02, held in conjunction with CP02, Ithaca, NY).

[46] Allen Van Gelder.  Verifying RUP proofs of propositional unsatisfiability.  In Tenth In-

ternational Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, 2008.

http://isaim2008.unl.edu/index.php?page=proceedings.

[47] Allen Van Gelder. Improved conflict-clause minimization leads to improved propositional proof traces. In Twelfth International Conference on Theory and Applications of Satisfiability Testing, pages 141–146, Swansea, Wales, 2009.

[48] Allen Van Gelder. Vortex core detection: Back to basics. In Proceedings of SPIE Conference on Visualization and Data Analysis, San Francisco, California, 2012.

[49] Allen Van Gelder and Kwansik Kim. Direct volume rendering with shading via 3D textures. In ACM/IEEE Symposium on Volume Visualization, San Francisco, CA, October 1996. See also technical report UCSC-CRL-96-16.

[50] Allen Van Gelder and Fumiaki Okushi. Lemma and cut strategies for propositional model elimination. Annals of Mathematics and Artificial Intelligence, 26(1–4):113–132, 1999.

[51] Allen Van Gelder and Fumiaki Okushi. A propositional theorem prover to solve planning and other problems. Annals of Mathematics and Artificial Intelligence, 26(1–4):87–112, 1999.

[52] Allen Van Gelder and Alex Pang. Using PVsolve to analyze and locate positions of parallel vectors. IEEE Transactions on Visualization and Computer Graphics, 15((in press)), 2009. (preprint at

http://www.cse.ucsc.edu/ ∼avg/Papers/ pvsolve-preprint.pdf).

[53] Allen Van Gelder and Alex Pang. Using PVsolve to analyze and locate positions of parallel vectors. IEEE Transactions on Visualization and Computer Graphics, 15:682–695, 2009.

[54] Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3):620–650, 1991. Preliminary abstract appeared in 1988 (7th) ACM Symposium on Principles of Database Systems.

[55] Allen Van Gelder and John S. Schlipf. Common-sense axiomatizations for logic programs. Journal of Logic Programming, 17(2-4):161–195, 1993.

[56] Allen Van Gelder and Ivor Spence. Zero-one designs produce small hard sat instances. In Thirteenth International Conference on Theory and Applications of Satisfiability Testing, Edinburgh, Scotland, 2010.

[57] Allen Van Gelder and Rodney W. Topor. Safety and correct translation of relational calculus formulas. In 6th ACM Symp. on Principles of Database Systems, 1987.

[58] Allen Van Gelder and Rodney W. Topor. Safety and translation of relational calculus formulas. ACM Transactions on Database Systems, 16(2):235–278, 1991.

[59] Allen Van Gelder and Yumi K. Tsuji. Incomplete thoughts about incomplete satisfiability procedures. In Second DIMACS Challenge Workshop: Cliques, Coloring and Satisfiability, October 1993.

[60] Allen Van Gelder and Yumi K. Tsuji. Satisfiability testing with more reasoning and less guessing. In D. S. Johnson and M. Trick, editors, Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge., DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1996. (Appendix has Tutorial on Statistics in Satisfiability Research).

[61] Allen Van Gelder, Vivek Verma, and Jane Wilhelms. Volume decimation of irregular tetrahedral grids. In Computer Graphics International Proceedings, Canmore, Alberta, Canada, June 1999.

[62] Allen Van Gelder and Jane Wilhelms. Interactive Animated Visualization of Flow Fields. In 1992 Workshop on Volume Visualization, pages 47–54, Boston, Mass., October 1992. ACM.

[63] Allen Van Gelder and Jane Wilhelms. Interactive animated visualization of flow fields. In 1992 Workshop on Volume Visualization, pages 47–54, Boston, Mass., 1992. ACM.

[64] Allen Van Gelder and Jane Wilhelms. Rapid exploration of curvilinear grids using direct volume rendering. In Visualization ’93, San Jose, CA, October 1993. IEEE. (extended abstract) Also, University of California technical report UCSC-CRL-93-02.

[65] Allen Van Gelder and Jane Wilhelms. Doing it with mirrors: Low budget stereo graphics. In IS&TSPIE Electronic Imaging: Science and Technology, pages 68–77, February 7–8 1994. Also University of California technical report UCSC-CRL-93-22.

[66] Allen Van Gelder and Jane Wilhelms. Topological considerations in isosurface generation. ACM Transactions on Graphics, 13(4):337–375, October 1994. Corrigendum with color pictures appears in July 1995 issue (14(3):307– 308).

[67] Allen Van Gelder and Jane Wilhelms. An interactive fur modeling technique. In Proceedings of Graphics Interface, May 1997.

[68] Tino Weinkauf, Holger Theisel, Allen Van Gelder, and Alex Pang. Stable feature flow fields. IEEE Transactions on Visualization and Computer Graphics, 17(6):770–780, 2011. (also at http://www.cse.ucsc.edu/

∼avg/Papers/ stableFFF.pdf).

[69] Jane Wilhelms and Allen Van Gelder. Octrees for faster isosurface generation. ACM Transaction on Graphics, 11(3):201–227, July 1992.

[70] Jane Wilhelms and Allen Van Gelder. A coherent projection approach for direct volume rendering. Computer Graphics (ACM Siggraph Proceedings), 25(4):275–284, 1991.

[71] Jane Wilhelms and Allen Van Gelder. Multi-dimensional trees for controlled volume rendering and compression. In ACM Symposium on Volume Visualization 1994, pages 27–34, Washington, D.C., October 1994. See also technical report UCSC-CRL-94-02.

[72] Jane Wilhelms and Allen Van Gelder. Anatomically based modeling. In Computer Graphics, pages 173–180, Los Angeles, Ca., August 1997. ACM Siggraph Conference Proceedings.

[73] Jane Wilhelms and Allen Van Gelder. Efficient spherical joint limits with reach cones. Technical report, UCSC, April 2001. Available at

http://www.acm.org/jgt; includes C code.

[74] Jane Wilhelms and Allen Van Gelder. Fast and easy reach-cone joint limits. Journal of Graphics Tools, 6(2):27– 41, 2001.

[75] Jane Wilhelms and Allen Van Gelder. Combining vision and computer graphics for video motion capture. The Visual Computer, 2002.

[76] Jane Wilhelms and Allen Van Gelder. Interactive video-based motion capture for character animation. In IASTED Conference on Computer Graphics and Imaging, Kauai, Hawaii, August 2002.

[77] Jane Wilhelms, Allen Van Gelder, Leon Atkinson-Derman, and Alison Luo. Human motion from active contours. In IEEE Workshop on Human Motion, December 2000.

[78] Jane Wilhelms, Allen Van Gelder, Paul Tarantino, and Jonathon Gibbs. Hierarchical and parallelizable direct volume rendering for irregular and multiple grids. In IEEE Visualization ’96 Conference Proceedings, pages 57–64, October 1996.