% ==> aggll-preprint.bib <==
@INPROCEEDINGS(	VG93-dood,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Foundations of Aggregation in Deductive Databases",
	BOOKTITLE = "Third International Conference on
		Deductive and Object-Oriented Databases",
	ADDRESS = "Phoenix, AZ",
	MONTH = dec,
	YEAR = "1993" )


% ==> altfpjcss.bib <==
@ARTICLE(	VG93-jcss,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "The Alternating Fixpoint of Logic Programs with Negation",
	JOURNAL = "Journal of Computer and System Sciences",
	volume = 47, number = 1,
	pages = "185--221",
	YEAR = "1993",
	ANNOTE = "Preliminary abstract appeared in
		Eighth {ACM} Symposium on Principles of Database Systems,
		1989."
	)


% ==> amai04.bib <==
@ARTICLE{OkushiVanGelder04-AMAI-persistent,
	Author = "Okushi, Fumiaki and Van Gelder, Allen",
	Title = "Persistent and Quasi-Persistent Lemmas
		in Propositional Model Elimination",
  journal =	"Annals of Mathematics and Artificial Intelligence",
  volume =	"40",
  number =	"3--4",
  pages = 	"373--402",
  year =	 2004
	}


% ==> ambig94.bib <==
@ARTICLE{VanGelder94a,
	AUTHOR	= "Van Gelder, Allen and Wilhelms, Jane",
	TITLE	= "Topological Considerations in Isosurface Generation",
	JOURNAL = "ACM Transactions on Graphics",
	YEAR	= "1994",
	MONTH	= "October",
	VOLUME	= "13",
	NUMBER	= "4",
        PAGES   = "337--375",
        NOTE    = "Corrigendum with color pictures appears in July 1995 issue
                  (14(3):307--308).",
        ANNOTE  = "Journal version of 1990 Vol Vis workshop paper."
	}


% ==> anatomy97.bib <==
@INPROCEEDINGS{Wilhelms97,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE	= "Anatomically Based Modeling",
	BOOKTITLE = "Computer Graphics",
	YEAR	= "1997",
	EDITOR	= "",
	PAGES	= "173--180",
	ORGANIZATION = "ACM Siggraph Conference Proceedings",
	PUBLISHER = "",
	ADDRESS	= "Los Angeles, Ca.",
	MONTH	= "August",
	NOTE	= "",
	ANNOTE	= ""
	}


% ==> aut-jar-dist.bib <==
@ARTICLE{VanGelder-aut-modoc-JAR,
  author = 	 "Van Gelder, Allen",
  title = 	 "Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy",
  journal = 	 "Journal of Automated Reasoning",
  year = 	 "1999",
  volume = 	 "23",
  number = 	 "2",
  pages = 	 "137--193"
}


% ==> careful.bib <==
@inproceedings{VG-careful-SAT11,
   author = "Van Gelder, A.",
   title = "Careful Ranking of Multiple Solvers with Timeouts and Ties",
   booktitle = "Proc.\ SAT (LNCS 6695)",
   pages = "317--328",
   publisher = "Springer",
   year      = "2011"
}


% ==> ccmin-avg-sat09.bib <==
@INPROCEEDINGS{VanGelder-sat2009,
        Author = "Van Gelder, Allen",
        Title = "Improved Conflict-Clause Minimization Leads to
		Improved Propositional Proof Traces",
        BOOKTITLE = "Twelfth International Conference on
		Theory and Applications of Satisfiability Testing",
        PAGES = "141--146",
        ADDRESS = "Swansea, Wales",
        YEAR = "2009"
        }


% ==> chu91.bib <==
@ARTICLE(	VG91-chu,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Deriving Constraints Among Argument Sizes in Logic Programs",
	JOURNAL = "Annals of Mathematics and Artificial Intelligence",
	VOLUME = "1",
	NUMBER = "3",
	PAGES = "361--392",
	YEAR = "1991"	)


% ==> colorsat02.bib <==
@ARTICLE{    VG07-colorsat-DAM,
	AUTHOR = "Van Gelder, Allen",
	Title = "Another Look at Graph Coloring via
			Propositional Satisfiability",
	JOURNAL = "Discrete Applied Mathematics",
	VOLUME = "156", NUMBER = 2,
	PAGES = "230--243",
	NOTE = "(Preliminary version appeared in COLOR02,
		held in conjunction with CP02, Ithaca, NY)",
	MONTH = jan,
	YEAR = 2008
	}


% ==> colorsat07.bib <==
@ARTICLE{    VG07-colorsat-DAM,
	AUTHOR = "Van Gelder, Allen",
	Title = "Another Look at Graph Coloring via
			Propositional Satisfiability",
	JOURNAL = "Discrete Applied Mathematics",
	VOLUME = "156", NUMBER = 2,
	PAGES = "230--243",
	NOTE = "(Preliminary version appeared in COLOR02,
		held in conjunction with CP02, Ithaca, NY)",
	MONTH = jan,
	YEAR = 2008
	}


% ==> cover-number-short.bib <==
@INPROCEEDINGS{VanGelder-SAT06,
        Author = "Van Gelder, Allen",
        Title = "Preliminary Report on Input Cover Number as
		a Metric for Propositional Resolution Proofs",
        BOOKTITLE = "Theory and Applications of Satisfiability Testing,
		(SAT), LNCS 4121",
        PAGES = "48--53",
        ADDRESS = "Seattle, WA",
        YEAR = "2006"
        }


% ==> cover-number.bib <==
@INPROCEEDINGS{VanGelder-SAT06,
        Author = "Van Gelder, Allen",
        Title = "Preliminary Report on Input Cover Number as
		a Metric for Propositional Resolution Proofs",
        BOOKTITLE = "Theory and Applications of Satisfiability Testing,
		(SAT), LNCS 4121",
        PAGES = "48--53",
        ADDRESS = "Seattle, WA",
        YEAR = "2006"
        }


% ==> ddgen93.bib <==
@INPROCEEDINGS(	PVK93-ddgen,
	AUTHOR = "Post, Kjell and Van Gelder, Allen and Kerr, James",
	TITLE = "Deterministic Parsing of Languages with Dynamic Operators",
	BOOKTITLE = "International Logic Programming Symposium",
	YEAR = "1993", MONTH = oct )


% ==> decimation-cgi99.bib <==
@INPROCEEDINGS{VanGelder99,
	AUTHOR	= "Van Gelder, Allen and Vivek Verma and Jane Wilhelms",
	TITLE	= "Volume Decimation of Irregular Tetrahedral Grids",
	BOOKTITLE = "Computer Graphics International Proceedings",
	YEAR	= "1999",
	MONTH	= "June",
	ADDRESS	= "Canmore, Alberta, Canada"
	}


% ==> eff-p-sim-aaai08.bib <==
@INPROCEEDINGS{Hertel-AAAI08,
	AUTHOR	= "Philipp Hertel and Fahiem Bacchus and Toniann Pitassi and
		Van Gelder, Allen",
	AUTHORSHORT	= "P. Hertel and F. Bacchus and T. Pitassi and
		Van Gelder, A.",
	TITLE	= "Clause Learning Can Effectively P-Simulate
		General Propositional Resolution",
	BOOKTITLE = "Twenty-Third AAAI Conference on Artificial Intelligence
		(AAAI-08)",
	YEAR	= "2008",
	MONTH	= jul,
	PAGES	= "283--290",
	ORGANIZATION = "AAAI",
	ADDRESS	= "Chicago"
	}


% ==> elastic-tools-1.bib <==
@ARTICLE{VanGelder98,
	AUTHOR	= "Van Gelder, Allen",
	TITLE	= "Approximate Simulation of Elastic Membranes by
                  Triangulated Spring Meshes",
	YEAR	= "1998",
	VOLUME = "3",
	NUMBER = "2",
	PAGES = "21--42",
	JOURNAL = "Journal of Graphics Tools",
	ANNOTE	= "",
	}


% ==> flow92.bib <==
@INPROCEEDINGS{VanGelder92,
	AUTHOR	= "Van Gelder, Allen and Jane Wilhelms",
	TITLE	= "Interactive {A}nimated {V}isualization of {F}low {F}ields",
	BOOKTITLE = "1992 Workshop on Volume Visualization",
	YEAR	= "1992",
	PAGES	= "47--54",
	MONTH	= "October",
	ORGANIZATION = "ACM",
	ADDRESS	= "Boston, Mass."
	}


% ==> franco-vg.bib <==
@ARTICLE{FVG03-matching,
	AUTHOR = "Franco, John and Van Gelder, Allen",
	TITLE  = "A Perspective on Certain Polynomial Time Solvable
		Classes of Satisfiability",
	JOURNAL = "Discrete Applied Mathematics",
	VOLUME = "125",
	NUMBER = "2--3",
	PAGES = "177--214",
	YEAR = 2003
	}


% ==> fs02.bib <==
@ARTICLE{Wilhelms02fs,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE	= "Combining Vision and Computer Graphics for Video
			Motion Capture",
	JOURNAL = "The Visual Computer",
	NUMBER	= "",
	VOLUME  = "",
	PAGES	= "",
	MONTH	= "",
        ADDRESS = "",
	YEAR	= "2002"
	}


% ==> fur_gi.bib <==
@INPROCEEDINGS{VanGelder97fur,
	AUTHOR  = "Van Gelder, Allen and Jane Wilhelms",
	TITLE   = "An Interactive Fur Modeling Technique",
	BOOKTITLE = "Proceedings of Graphics Interface",
	YEAR    = "1997",
	PAGES   = "",
	ORGANIZATION = "",
	PUBLISHER = "", 
	ADDRESS = "",
	MONTH = "May",
	NOTE = "",
	ANNOTE = ""
	}


% ==> generalized.bib <==
@inproceedings{VG-generalized-SAT11,
   author = "Van Gelder, A.",
   title = "Generalized Conflict-Clause Strengthening
                for Satisfiability Solvers",
   booktitle = "Proc.\ SAT (LNCS 6695)",
   pages = "329--342",
   publisher = "Springer",
   year      = "2011"
}


% ==> gg95.bib <==
@INCOLLECTION{VanGelder95-GG-V,
        AUTHOR  = "Van Gelder, Allen",
        BOOKTITLE       = "Graphics Gems V",
        TITLE   = "Efficient Computation of Polygon Area
                and Polyhedron Volume",
        PAGES   = "",
        PUBLISHER = "Academic Press",
        YEAR    = "1995",
        ADDRESS = "Boston, Mass.",
        NOTE    = "",
        ANNOTE  = ""
        }


% ==> hawaii02.bib <==
@INPROCEEDINGS{Wilhelms02hawaii,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE	= "Interactive Video-Based Motion Capture for Character Animation",
	BOOKTITLE = "IASTED Conference on Computer Graphics and Imaging",
	YEAR	= "2002",
	PAGES	= "",
	MONTH	= "August",
        ADDRESS = "Kauai, Hawaii",
	NOTE	= "",
	ANNOTE	= ""
	}


% ==> human00.bib <==
@INPROCEEDINGS{Wilhelms00,
  AUTHOR	= "Jane Wilhelms and Van Gelder, Allen
	and Leon Atkinson-Derman and Alison Luo",
  TITLE	= "Human Motion from Active Contours",
  BOOKTITLE = "IEEE Workshop on Human Motion",
  EDITOR	= "",
  PAGES	= "",
  ORGANIZATION = "",
  PUBLISHER = "",
  ADDRESS	= "",
  MONTH	= "December",
  YEAR	= "2000"
}


% ==> incomplete.bib <==
@inproceedings{VanGelderTsuji93,
 Author = "Van Gelder, Allen and Tsuji, Yumi K.",
 Title = "Incomplete Thoughts about Incomplete Satisfiability Procedures",
 Year = 1993,
 Month = "October",
 BOOKTitle = "Second DIMACS Challenge Workshop:
             Cliques, Coloring and Satisfiability",
 ANNOTE = "{Abstract: 
 Recent successes with incomplete satisfiability procedures raise numerous
 issues about their uses and evaluation.  Most such procedures search
 for "yes" answers, and give up if they do not find one.  The need for 
 "no" answers as well is addressed.  It is shown that a recent 
 approximation algorithm of Yannakakis can produce "no" answers only in 
 somewhat trivial cases.  The possibility of salvaging information from
 a "yes" program that is giving up, and using it to find a "no" answer
 is discussed.
 Two incomplete procedures were studied experimentally.
 One (based on "easy" resolutions) produces "no" answers.
 The other (based on Johnson's maximum satisfiability approximation
 algorithm) produces "yes" answers.  Both are deterministic, polynomial time
 algorithms, quadratic with careful implementation.  Combined, they
 solved 83\% of the formulas generated from a circuit-based applications,
 ranging from 400 to over 10000 variables.
 }"
}


% ==> input-dist.bib <==
@INPROCEEDINGS{VanGelder-sat2005,
        Author = "Van Gelder, Allen",
        Title = "Input Distance and Lower Bounds for
		Propositional Resolution Proof Length",
        BOOKTITLE = "Eighth International Conference on
		Theory and Applications of Satisfiability Testing",
        PAGES = "",
        ADDRESS = "St.\ Andrews, Scotland",
        YEAR = "2005"
        }


% ==> jacm88.bib <==
@ARTICLE(       UV88b,
	AUTHOR = "Ullman, Jeffrey D. and Van Gelder, Allen",
	TITLE = "Efficient tests for top-down termination of logical rules",
	JOURNAL = "Journal of the ACM",
	VOLUME = "35", NUMBER = "2",
	PAGES = "345--373",
	URL = "http://portal.acm.org/citation.cfm?id=42285",
	NOTE = "(Preprint available from second author)",
	YEAR = "1988"   )


% ==> jlp87.bib <==
@ARTICLE(	VG87a,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Efficient loop detection in {P}rolog using the
		tortoise and hare technique",
	JOURNAL = "Journal of Logic Programming",
	VOLUME = "4", NUMBER = "1",
	YEAR = "1987",
	PAGES = "23--33"	)


% ==> jlp89.bib <==
@ARTICLE(	VG89a,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Negation as Failure Using Tight Derivations for
		General Logic Programs",
	JOURNAL = "Journal of Logic Programming",
	VOLUME = "6", NUMBER = "1",
	YEAR = "1989",
	NOTE = "Preliminary versions appeared in
		{\it Third IEEE Symp.~on Logic Programming} (1986), and
		{\it Foundations of Deductive Databases and Logic Programming},
		J.~Minker, ed., Morgan Kaufmann, 1988.",
	PAGES = "109--133"	)


% ==> jlp90.bib <==
@ARTICLE(	VG90a,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Modeling simultaneous events with
		default reasoning and tight derivations",
	JOURNAL = "Journal of Logic Programming",
	VOLUME = "8", NUMBER = "1",
	YEAR = "1990",
	PAGES = "41--52"	)


% ==> jtl-tr.bib <==
@TECHREPORT{Wilhelms01jt-tr-jgt,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE	= "Efficient Spherical Joint Limits with Reach Cones",
	INSTITUTION = "UCSC",
	NUMBER	= "",
	YEAR	= "2001",
	PAGES	= "",
	MONTH	= "April",
        ADDRESS = "",
	NOTE	= "Available at\newline
		{\tt http://www.acm.org/jgt; includes C code.}",
	ANNOTE	= ""
	}


% ==> jtl.bib <==
@ARTICLE{Wilhelms00jt,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE	= "Fast and Easy Reach-Cone Joint Limits",
	JOURNAL = "Journal of Graphics Tools",
	NUMBER	= "2",
	VOLUME  = "6",
	YEAR	= "2001",
	PAGES	= "27--41",
	MONTH	= "",
        ADDRESS = "",
	ANNOTE	= "Available at\newline
		{\tt ftp://ftp.cse.ucsc.edu/pub/avg/jtl.pdf.}",
	NOTE	= ""
	}


% ==> kclose-tr.bib <==
@inproceedings{VanGelderTsuji96,
 Author = "Van Gelder, Allen and Tsuji, Yumi K.",
 Title = "Satisfiability Testing with More Reasoning and Less Guessing",
 Year = 1996,
 Editor = "Johnson, D. S. and Trick, M.",
 Publisher = "American Mathematical Society",
 Series = "DIMACS Series in Discrete Mathematics and Theoretical Computer
        Science", 
 BookTitle = "Cliques, Coloring, and Satisfiability: 
       Second DIMACS Implementation Challenge.", 
 NOTE = "(Appendix has Tutorial on Statistics in Satisfiability Research)",
 ANNOTE ="{Abstract: 
 A new algorithm for testing satisfiability of propositional formulas in 
 conjunctive normal form (CNF) is described.  It applies reasoning in the 
 form of certain resolution operations, and identification of equivalent 
 literals.  Resolution produces growth in the size of the formula, but within 
 a global quadratic bound; most previous methods avoid operations that 
 produce any growth, and generally do not identify equivalent literals.
 Computational experience so far suggests that the method does substantially
 less "guessing" than previously reported algorithms, while keeping a 
 polynomial time bound on the work done between guesses.  However, the
 time trade-off between reasoning and guessing is not yet clear.
 }",
 ANNOTE2="{
 We present experimental data comparing six branching strategies of the 
 proposed algorithm on a variety of problems, including several Dimacs
 benchmarks.  These branching strategies were shown to be different with 
 statistical significance and a new scheme based on Johnson's maximum 
 satisfiability approximation algorithm was the best on random 3-CNF formulas.
 In addition to the choice of a branching strategy, we found that 
 {\it variable reordering} can significantly impact the performance for many
 classes of problems in the Dimacs benchmark.  We have also tested both 
 satisfiable and unsatisfiable random 3-CNF formulas with 50-283 variables
 and 4.27 ratio of clauses to variables;  this class is generally acknowledged 
 to be relatively "hard" and required extensive backtracking by other 
 algorithms.  The new algorithm has solved them with surprisingly little 
 backtracking: for 200 variables at this ratio, the average number of guesses
 was 2,955 and the average CPU time was 119 seconds on SunSS10/41.  
 }",
 ANNOTE3="{
 For 283 variables, the average number of guesses was 57,503 with the
 values ranging from 105 to 182,006 in a set of 100 random formulas.
 We have also observed that unsatisfiable random problems do not follow the
 easy-hard-easy pattern.
 Our results indicate an exponential growth rate of
 $2^{.004L}$ for random formulas,
 where $L$ is the number of \emph{occurrences} of
 literals in the formula.
 Larger unsatisfiable formulas from circuit-fault analysis, with 500--10400
 variables were solved with \emph{no} backtracking in some cases.
 }"
}


% ==> leaner05.bib <==
@ARTICLE{VanGelder05-leaner,
  author = 	 "Van Gelder, Allen",
	Title = "Toward Leaner Binary-Clause Reasoning in a
		Satisfiability Solver",
  journal =	"Annals of Mathematics and Artificial Intelligence",
  volume =	"43",
  number =	"1--4",
  pages = 	"239--253",
  NOTE =	"(Preliminary version appeared in SAT02, Cincinnati)",
  year =	 2005
}


% ==> lemmas-dist.bib <==
@ARTICLE{VanGelderOkushi99-AMAI-Lemmas,
  author = 	 "Van Gelder, Allen and Fumiaki Okushi",
  title = 	 "Lemma and Cut Strategies for Propositional Model Elimination",
  journal =	"Annals of Mathematics and Artificial Intelligence",
  volume =	"26",
  number =	"1--4",
  pages = 	"113--132",
  year =	 1999
}


% ==> lics01-sat.bib <==
@INPROCEEDINGS{VG01-lics-sat,
	Author = "Van Gelder, Allen",
	Title = "Combining Preorder and Postorder Resolution
		in a Satisfiability Solver",
	BOOKTITLE = "IEEE/ASL LICS Satisfiability Workshop",
	PUBLISHER = "",
	ADDRESS = "Boston",
	PAGES = "",
	YEAR = "2001"
	}


% ==> mdh94.bib <==
@INPROCEEDINGS{Wilhelms94b,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen",
	TITLE   = "Multi-Dimensional Trees for Controlled Volume
		Rendering and Compression",
	BOOKTITLE = "ACM Symposium on Volume Visualization 1994",
	MONTH	= "October",
	ADDRESS = "Washington, D.C.",
	NOTE	= "See  also technical report UCSC-CRL-94-02",
	PAGES	= "27--34",
	YEAR	= "1994"
	}


% ==> mirrors94.bib <==
@INPROCEEDINGS{VanGelder94,
	AUTHOR	= "Van Gelder, Allen and Jane Wilhelms",
	TITLE	= "Doing It with Mirrors: Low Budget Stereo Graphics",
	BOOKTITLE = "IS\&T\/SPIE Electronic Imaging: Science and
		Technology",
	YEAR	= "1994",
	MONTH   = "February 7--8",
	PAGES	= "68--77",
	NOTE	= "Also University of California technical
		report UCSC-CRL-93-22",
	ANNOTE	= "UCSC CIS Department,
		Applied Sciences Building, Santa Cruz, CA 95064"
	}


% ==> modoc-ub-dist.bib <==
@ARTICLE{    VG97-modoc-ub-DAM,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "Complexity Analysis of  Propositional Resolution
		with Autarky Pruning",
	JOURNAL = "Discrete Applied Mathematics",
	VOLUME = "96--97",
	PAGES = "195--221",
	YEAR = 1999
	}


% ==> nail86.bib <==
@INPROCEEDINGS(	MUV86,
	AUTHOR = "Morris, K. and Ullman, J. D. and Van Gelder, A.",
	TITLE = "Design overview of the {Nail!} system",
	BOOKTITLE = "Third Int'l Conf.\ on Logic Programming",
	PAGES = "554--568",
	YEAR = "1986")


% ==> need-proofs.bib <==
@INPROCEEDINGS{VG02-cfv,
	Author = "Van Gelder, Allen",
	Title = "Decision Procedures Should Be Able to Produce
			(Easily) Checkable Proofs",
	BOOKTITLE = "Workshop on Constraints in Formal Verification",
	PUBLISHER = "",
	ADDRESS = "Ithaca, NY",
	PAGES = "",
	YEAR = "2002",
	NOTE = "(in conjunction with CP02)",
	ANNOTE = "Abstract:
	"
	}


% ==> oct92.bib <==
@article{WVG92,
        author = "Jane Wilhelms and Allen Van Gelder",
        title = "Octrees for Faster Isosurface Generation",
        journal = "ACM Transaction on Graphics",
        volume = "11",
        number = "3",
        month = "July",
        year = "1992",
        pages = "201--227"}


% ==> packet89.bib <==
@ARTICLE(       VG89c,
	AUTHOR = "David Peleg and Van Gelder, Allen",
	TITLE = "Packet Distribution on a Ring",
	JOURNAL = "Journal of Parallel and Distributed Computing",
	VOLUME = "6", NUMBER = "3",
	PAGES = "558--567",
	YEAR = "1989"   )


% ==> parallel88.bib <==
@ARTICLE(       UV88a,
	AUTHOR = "Ullman, Jeffrey D. and Van Gelder, Allen",
	TITLE = " Parallel Complexity of Logical Query Programs",
	JOURNAL = "Algorithmica",
	VOLUME = "3", NUMBER = "1",
	PAGES = "5--42",
	URL = "http://www.springerlink.com/content/un5uju4pj430175w/",
	NOTE = "(Preprint available from second author. Short version
		appeared in FOCS, 1986.)",
	YEAR = "1988"   )


% ==> partition-IC.bib <==
@ARTICLE{    PVG97-partition-IC,
	AUTHOR = "Park, Tai Joon and Van Gelder, Allen",
	TITLE = "Partitioning Methods for Satisfiability Testing
			on Large Formulas",
	JOURNAL = "Information and Computation",
	VOLUME = "161", NUMBER = "2",
	NOTE = "(Extended abstract, full paper appeared in CADE-13)",
	YEAR = 2000
	}


% ==> partition-cade13.bib <==
@INPROCEEDINGS{ParkVanGelder96,
AUTHOR          = "Park, Tai Joon and Van Gelder, Allen",
TITLE           = "Partitioning  Methods for Satisfiability Testing
                  on Large Formulas",
BOOKTITLE       = "Proceedings 13th International Conference on
                  Automated Deduction",
PUBLISHER       = "Springer-Verlag",
SERIES          = "LNAI",
VOLUME          = "1104",
PAGES           = "748--762",
MONTH           = "July",
YEAR            = "1996"
		}


% ==> planning-dist.bib <==
@ARTICLE{VanGelderOkushi98-AMAI-Planning,
  author = 	 "Van Gelder, Allen and Fumiaki Okushi",
  title = 	 "A Propositional Theorem Prover to Solve Planning
			and Other Problems",
  journal =	"Annals of Mathematics and Artificial Intelligence",
  volume =	"26",
  number =	"1--4",
  pages = 	"87--112",
  year =	 1999
}


% ==> pods92.bib <==
@INPROCEEDINGS(	VG92-pods,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "The well-founded semantics of aggregation",
	BOOKTITLE = "{ACM} Symposium on Principles of Database Systems",
	YEAR = "1992" )


% ==> poly-res.bib <==
@INPROCEEDINGS{VanGelder98-nondecisive-SAIM,
	Author = "Van Gelder, Allen",
	Title = "Propositional Search with $k$-Clause Introduction
		Can Be Polynomially Simulated by Resolution",
	BOOKTITLE = "(Electronic) Proc.\ 5th Int'l Symposium on
		Artificial Intelligence and Mathematics",
	ANNOTE = "{\tt http://rutcor.rutgers.edu/\~{}amai}",
	YEAR = "1998"
	}


% ==> pool-res.bib <==
@INPROCEEDINGS{VanGelder-LPAR05,
        Author = "Van Gelder, Allen",
        Title = "Pool Resolution and Its Relation to Regular Resolution and
		{DPLL} with Clause Learning",
        BOOKTITLE = "Logic for Programming, Artificial Intelligence,
		and Reasoning (LPAR), LNAI 3835",
        PAGES = "580--594",
	PUBLISHER = "Springer-Verlag",
        ADDRESS = "Montego Bay, Jamaica",
        YEAR = "2005"
        }


% ==> pram89.bib <==
@ARTICLE(       VG89b,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "PRAM Processor Allocation: A Hidden Bottleneck
		in Sublogarithmic Algorithms",
	JOURNAL = "IEEE Transactions on Computers",
	VOLUME = "38", NUMBER = "2",
	PAGES = "289--292",
	YEAR = "1989"   )


% ==> proj91.bib <==
@article{WVG91,
	author	= {Jane Wilhelms AND Van Gelder, Allen},
	title	= {A Coherent Projection Approach for Direct
		Volume Rendering},
	journal = {Computer Graphics (ACM Siggraph Proceedings)},
	year	= {1991},
	volume	= {25},
	number	= {4},
	pages	= {275--284}
	}


% ==> proofs-isaim08.bib <==
@INPROCEEDINGS{VanGelder-ISAIM08,
        Author = "Van Gelder, Allen",
        Title = "Verifying {RUP} Proofs of Propositional Unsatisfiability",
        BOOKTITLE = "Tenth International Symposium on
		Artificial Intelligence and Mathematics",
        PAGES = "",
        ADDRESS = "Fort Lauderdale",
	NOTE = "{\texttt{http://isaim2008.unl.edu/index.php?page=proceedings}}",
        YEAR = "2008"
        }

% ==> proofs-sat07.bib <==
@INPROCEEDINGS{VanGelder-sat2007,
        Author = "Van Gelder, Allen",
        Title = "Verifying Propositional Unsatisfiability:
		Pitfalls to Avoid",
        BOOKTITLE = "Tenth International Conference on
		Theory and Applications of Satisfiability Testing",
        PAGES = "",
        ADDRESS = "Lisboa, Portugal",
        YEAR = "2007"
        }


% ==> pvsolve-preprint.bib <==
@ARTICLE{       VGP-tvcg09,
    AUTHOR = "Van Gelder, Allen and Pang, Alex",
    TITLE = "Using {PVsolve} to Analyze and Locate Positions of Parallel Vectors",
    JOURNAL = "IEEE Transactions on Visualization and Computer Graphics",
    VOLUME = "15", NUMBER = "(in press)",
    PAGES = "",
    NOTE =  "(preprint at
    \texttt{http://www.cse.ucsc.edu/ $\sim$avg/Papers/ pvsolve-preprint.pdf})",
    YEAR = "2009"
    }


% ==> pvsolve.bib <==
@ARTICLE{VGP09-TVCG,
	AUTHOR	= "Van Gelder, Allen and Pang, Alex",
	TITLE	= "Using {PVsolve} to Analyze and Locate Positions of Parallel Vectors",
	JOURNAL = "IEEE Transactions on Visualization and Computer Graphics",
	YEAR	= "2009",
	VOLUME	= "15",
	PAGES	= "682--695",
	NOTE	= "",
	ANNOTE	= ""
	}


% ==> rjcfTR.bib <==
@techreport{VG09-rjcf-TR,
   author =  "Van Gelder, A.",
   authorlong =  "Van Gelder, Allen",
   title = "Report on Relaxed {J}ordan Canonical Form for Computer Animation and Visualization",
   institution = "UC Santa Cruz",
   note =  "(URL:
\texttt{http://www.cse.ucsc.edu/ $\sim$avg/Papers/ rjcfTR.pdf})",
     year     = "2009",
     month    = "Jan."
}


% ==> safety87.bib <==
@INPROCEEDINGS(	VT87,
	AUTHOR = "Van Gelder, Allen and Topor, Rodney W.",
	TITLE = "Safety and correct translation of
		relational calculus formulas",
	BOOKTITLE = "6th {ACM} Symp.\ on Principles of Database Systems",
	YEAR = "1987",
	PAGES = ""	)


% ==> safety91.bib <==
@ARTICLE(	VT91,
	AUTHOR = "Van Gelder, Allen and Topor, Rodney W.",
	TITLE = "Safety and translation of relational calculus formulas",
	JOURNAL = "{ACM} Transactions on Database Systems",
	ANNOTE = "Extended abstract appeared in
		6th {ACM} Symp.\ on Principles of Database Systems.",
	VOLUME = "16",
	NUMBER = "2",
	PAGES = "235--278",
	YEAR = "1991"	)


% ==> sat-pre-post.bib <==
@INPROCEEDINGS{VG02-cbj-saim7,
	Author = "Van Gelder, Allen",
	Title = "Extracting (Easily) Checkable Proofs from a
		Satisfiability Solver that Employs both
		Preorder and Postorder Resolution",
	BOOKTITLE = "Seventh Int'l Symposium on AI and Mathematics",
	ADDRESS = "Ft.\ Lauderdale, FL",
	PAGES = "",
	YEAR = "2002"
	}


% ==> sat2000.bib <==
@INPROCEEDINGS{VanGelder-sat2000,
	Author = "Van Gelder, Allen",
	Title = "Lemmas in Propositional Model Search and
			Refutation Search",
	BOOKTITLE = "Third Workshop on the Satisfiability Problem",
	PAGES = "",
	ADDRESS = "Renesse, Netherlands",
	YEAR = "2000"
	}


% ==> satIC1988.bib <==
@Article{VanGelder88,
 Author="Van Gelder, Allen",
 Title="{A Satisfiability Tester for Non-Clausal Propositional Calculus}",
 Journal="Information and Computation",
 VOLUME=79,
 NUMBER=1,
 YEAR=1988,
 MONTH=oct,
 PAGES="1--21",
 ANNOTE="{
 An algorithm for satisfiability testing in the propositional calculus
 with a worst case running time that grows at a rate less than
 $2^{(0.25+\epsilon)L}$ is described, where $L$ is the length of the 
 input expression.  This represents a new upper bound on the complexity
 of non-clausal satisfiability testing.  The performance is achieved by 
 using lemmas concerning assignment and pruning that preserve
 satisfiability, together with choosing a "good" variable upon which
 to recur. For expressions in CNF, it is shown that an upper 
 bound is $2^{0.128L}$.
 }"
}


% ==> sgen2-sat10.bib <==
@INPROCEEDINGS{VanGelder-Spence-sat2010,
        Author = "Van Gelder, Allen and Spence, Ivor",
        Title = "Zero-One Designs Produce Small Hard SAT Instances",
        BOOKTITLE = "Thirteenth International Conference on
		Theory and Applications of Satisfiability Testing",
        PAGES = "",
        ADDRESS = "Edinburgh, Scotland",
        YEAR = "2010"
        }


% ==> sigmod86.bib <==
@INPROCEEDINGS(	VG86a,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "A message passing framework for logical query evaluation",
	BOOKTITLE = "1986 ACM-SIGMOD Conf.\ on Management of Data",
	YEAR = "1986",
	PAGES = "155--165"	)


% ==> stableFFF.bib <==
@ARTICLE{       WTVP-tvcg10,
    AUTHOR = "Weinkauf, Tino and Theisel, Holger and
                 Van Gelder, Allen and Pang, Alex",
    TITLE = "Stable Feature Flow Fields",
    JOURNAL = "IEEE Transactions on Visualization and Computer Graphics",
    VOLUME = "17", NUMBER = "6",
    PAGES = "770--780",
    NOTE =  "(also at
    \texttt{http://www.cse.ucsc.edu/ $\sim$avg/Papers/ stableFFF.pdf})",
    ANNOTE = "Abstract:
    Feature Flow Fields are a well-accepted approach for extracting and
    tracking features.  In particular, they are often used to track
    critical points in time-dependent vector fields and to extract and
    track vortex core lines.  The general idea is to extract the
    feature or its temporal evolution using a stream line integration
    in a derived vector field - the so-called Feature Flow Field
    (FFF).  Hence, the desired feature line is a stream line of the
    FFF. As we will carefully analyze in this paper, the stream lines
    around this feature line may diverge from it.  This creates an
    unstable situation: if the integration moves slightly off the
    feature line due to numerical errors, then it will be captured by
    the diverging neighborhood and carried away from the real feature
    line.  The goal of this paper is to define a new FFF with the
    guarantee that the neighborhood of a feature line has always
    converging behavior.  This way, we have an automatic correction of
    numerical errors: if the integration moves slightly off the feature
    line, it automatically moves back to it during the ongoing
    integration.  This yields results which are an order of magnitude
    more accurate than the results from previous schemes.  We present
    new stable FFF formulations for the main applications of tracking
    critical points and solving the Parallel Vectors operator.  We
    apply our method to a number of data sets.
    ",
    OPTmonth = "June",
    YEAR = "2011"   }


% ==> strategies.bib <==
@inproceedings{GVGB-strategies-IJCAI11,
   author = "A. Goultiaeva and and Van Gelder, A. and F. Bacchus",
   authorlong = "Alexandra Goultiaeva and Van Gelder, Allen and Fahiem Bacchus",
   title = "A Uniform Approach for Generating Proofs and Strategies for both
                True and False {QBF} Formulas",
   booktitle = "Proc.\ IJCAI",
   note = "(preprint at
\texttt{www.cse.ucsc.edu/\-$\tilde{\rule{2ex}{0pt}}$avg/\-Papers/\-strategies.pdf})",
   year      = "2011"
}


% ==> streamsurf01.bib <==
@INPROCEEDINGS{VanGelder-VisSym01,
	AUTHOR	= "Van Gelder, Allen",
	TITLE   = "Stream Surface Generation for Fluid Flow Solutions
		on Curvilinear Grids",
	BOOKTITLE = "Joint EUROGRAPHICS-IEEE TCVG Symposium on Visualization
		(VisSym01)",
	MONTH	= "May",
	ADDRESS = "Ascona, Switzerland",
	PAGES	= "",
	YEAR	= "2001"
	}


% ==> tensors-vg08-long.bib <==
@INPROCEEDINGS{Neeman-VG08,
	AUTHOR	= "Neeman, A. G. and Brannon, R. and Jeremi{\'c}, B. and
		Pang, A. and Van Gelder, A.",
	TITLE	= "Decomposition and Visualization of Fourth-Order
		Elastic-Plastic Tensors",
	BOOKTITLE = "IEEE/EG Symposium on Volume and Point-Based Graphics",
	YEAR	= "2008",
	MONTH	= aug,
	PAGES	= "",
	ORGANIZATION = "IEEE/EG",
	ADDRESS	= "Los Angeles"
	}


% ==> termab91.bib <==
@INPROCEEDINGS(	SV91-pods,
	AUTHOR = "Sohn, Kirack and Van Gelder, Allen",
	TITLE = "Termination Detection in Logic Programs
		using Argument Sizes",
	BOOKTITLE = "Tenth {ACM} Symposium on Principles of Database Systems",
	PAGES = "216--226",
	YEAR = "1991" )


% ==> vcore-vda12.bib <==
@INPROCEEDINGS {VG-vcore-vda12,
	AUTHOR = "Van Gelder, Allen",
	BOOKTITLE	= "Proceedings of SPIE Conference on
			Visualization and Data Analysis",
	TITLE	= "Vortex Core Detection: Back to Basics",
	optPAGES	= "--",
	optMONTH	= "January",
	ADDRESS	= "San Francisco, California",
	YEAR	= "2012",
	}


% ==> vis93.bib <==
@INPROCEEDINGS{VanGelder93a,
	AUTHOR	= "Van Gelder, Allen and Jane Wilhelms",
	TITLE	= "Rapid Exploration of Curvilinear Grids Using
		Direct Volume Rendering",
	BOOKTITLE = "Visualization '93",
	YEAR	= "1993",
	MONTH	= "October",
	ORGANIZATION = "{IEEE}",
	ADDRESS	= "San Jose, CA",
	NOTE = "(extended abstract) Also, University of
		California technical report UCSC-CRL-93-02",
	ANNOTE = "shorter version of VanGelder93"
	}


% ==> vis96.bib <==
@INPROCEEDINGS{Wilhelms96,
	AUTHOR	= "Jane Wilhelms and Van Gelder, Allen and Paul Tarantino and
	  Jonathon Gibbs",
	TITLE	= "Hierarchical and Parallelizable Direct Volume Rendering
	  for Irregular and Multiple Grids",
	YEAR	= "1996",
	PAGES	= "57--64",
	MONTH	= "October",
	BOOKTITLE = "IEEE Visualization '96 Conference Proceedings",
	ANNOTE	= ""
	}


% ==> voltx96.bib <==
@INPROCEEDINGS{VanGelderKim96,
	AUTHOR	= "Van Gelder, Allen and Kwansik Kim",
	TITLE	= "Direct Volume Rendering with Shading via {3D} Textures",
	BOOKTITLE = "{ACM/IEEE} Symposium on Volume Visualization",
	YEAR	= "1996",
	MONTH	= "October",
	ADDRESS	= "San Francisco, CA",
	NOTE	= "See  also technical report UCSC-CRL-96-16",
	}


% ==> volvis92.bib <==
@inproceedings
	{
	VGW92,
	author	= {Van Gelder, Allen AND Jane Wilhelms},
	title	= {Interactive Animated Visualization of Flow Fields},
	booktitle = {1992 Workshop on Volume Visualization},
	year	= {1992},
	pages	= {47--54},
	publisher = {ACM},
	address	= {Boston, Mass.}
	}


% ==> watched-lits.bib <==
@INPROCEEDINGS{VG02-watched-lits-saim7,
	Author = "Van Gelder, Allen",
	Title = "Generalizations of Watched Literals for Backtracking Search",
	BOOKTITLE = "Seventh Int'l Symposium on AI and Mathematics",
	INSTITUTION = "Univ.\ Calif., Santa Cruz",
	ADDRESS = "Ft.\ Lauderdale, FL",
	PAGES = "",
	YEAR = "2002"
	}


% ==> wf.bib <==
@ARTICLE(	VRS91,
	AUTHOR = "Van Gelder, Allen and Ross, Kenneth A. and Schlipf, John S.",
	TITLE = "The Well-Founded Semantics for General Logic Programs",
	JOURNAL = "Journal of the ACM",
	VOLUME = "38", NUMBER = "3",
	PAGES = "620--650",
	NOTE = "Preliminary abstract appeared in 1988
		(7th) {ACM} Symposium on Principles of Database Systems.",
	YEAR = "1991" )


% ==> wfax.bib <==
@ARTICLE{VS93-jlp,
	AUTHOR = "Van Gelder, Allen and Schlipf, John S.",
	TITLE = "Common-Sense Axiomatizations for Logic Programs",
	JOURNAL= "Journal of Logic Programming",
	VOLUME = 17, NUMBER = "2-4",
	YEAR = 1993,
	PAGES = "161--195"
	}


% ==> wfcircum90.bib <==
@TECHREPORT(VG90-circum,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "A New Form of Circumscription for Logic Programs",
	INSTITUTION = "Univ. of Calif.",
	ADDRESS = "Santa Cruz",
	NUMBER = "UCSC-CRL-90-50",
	NOTE = "Extended abstract in
		{\emph{Workshop on Logic Programming and Nonmonotonic
		Reasoning}} at 1990 NACLP",
	YEAR = 1990)


% ==> wftut.bib <==
@ARTICLE{VG98-wftut,
	AUTHOR = "Van Gelder, Allen",
	TITLE = "A Tutorial on the Well-Founded Semantics",
	JOURNAL= "Programmirovanie",
	VOLUME = 24, NUMBER = "1",
	YEAR = 1998,
	NOTE = "(Russian) Translation: Programming and Computer Software
		(24)1, Jan.~1998."
	}