Pratt V R
Two Easy Theories whose Combination is Hard Unpublished
1977, (Memo sent to Nelson and Oppen concerning a preprint of their paper citeNelsonO77).
Abstract | BibTeX
@unpublished{Pratt77, title = {Two Easy Theories whose Combination is Hard}, author = {V. R. Pratt}, year = {1977}, date = {1977-09-01}, abstract = {We restrict attention to the validity problem for unquantified disjunctions of literals (possibly negated atomic formulae) over the domain of integers, or what is just as good, the satisfiability problem for unquantified conjunctions. When $=$ is the only predicate symbol and all function symbols are left uninterpreted, or when $geq$ is the only predicate symbol (taking its standard interpretation on the integers) and the only terms are variables and integers, then satisfiability is decidable in polynomial time. However when $geq$ and uninterpreted function symbols are allowed to appear together, satisfiability becomes an NP-complete problem. This combination of the two theories can arise for example when reasoning about arrays (the uninterpreted function symbols) and subscript manipulation (where $geq$ arises in considering subscript bounds). These results are unaffected by the presence of successor, which also arises commonly in reasoning about subscript manipulation.}, note = {Memo sent to Nelson and Oppen concerning a preprint of their paper citeNelsonO77}, keywords = {}, pubstate = {published}, tppubtype = {unpublished} }
Close
Nelson G, Oppen D C
Fast Decision Algorithms based on Union and Find Proceedings Article
In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS'77), pp. 114–119, IEEE Computer Society Press, Providence, RI, USA, 1977, (The journal version of this paper is citeNelsonO80).
BibTeX
@inproceedings{NelsonO77, title = {Fast Decision Algorithms based on Union and Find}, author = {G. Nelson and D. C. Oppen}, year = {1977}, date = {1977-01-01}, booktitle = {Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS'77)}, pages = {114–119}, publisher = {IEEE Computer Society Press}, address = {Providence, RI, USA}, note = {The journal version of this paper is citeNelsonO80}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} }
Goldfarb D, Reid J K
A Practical Steepest-Edge Simplex Algorithm Journal Article
In: Mathematical Proramming, vol. 12, no. 1, pp. 361–371, 1977.
@article{GoldfarbR77, title = {A Practical Steepest-Edge Simplex Algorithm}, author = {D. Goldfarb and J. K. Reid}, year = {1977}, date = {1977-01-01}, journal = {Mathematical Proramming}, volume = {12}, number = {1}, pages = {361–371}, abstract = {It is shown that suitable recurrences may be used in order to implement in practice the steepest-edge simplex linear programming algorithm. In this algorithm each iteration is along an edge of the polytope of feasible solutions on which the objective function decreases most rapidly with respect to distance in the space of all the variables. Results of computer comparisons on medium-scale problems indicate that the resulting algorithm requires less iterations but about the same overall time as the algorithm of Harris [8], which may be regarded as approximating the steepest-edge algorithm. Both show a worthwhile advantage over the standard algorithm.}, keywords = {}, pubstate = {published}, tppubtype = {article} }
Cousot P, Cousot R
Static Determination of Dynamic Properties of Programs Proceedings Article
In: Robinet B (Ed.): Proceedings of the Second International Symposium on Programming, pp. 106–130, Dunod, Paris, France, Paris, France, 1976.
Abstract | Links | BibTeX
@inproceedings{CousotC76, title = {Static Determination of Dynamic Properties of Programs}, author = {P. Cousot and R. Cousot}, editor = {B. Robinet}, url = {http://www.di.ens.fr/~cousot/publications.www/CousotCousot-ISOP-76-Dunod-p106–130-1976.pdf}, year = {1976}, date = {1976-01-01}, booktitle = {Proceedings of the Second International Symposium on Programming}, pages = {106–130}, publisher = {Dunod, Paris, France}, address = {Paris, France}, abstract = {In high level languages, compile time type verifications are usually incomplete, and dynamic coherence checks must be inserted in object code. For example, in PASCAL one must dynamically verify that the values assigned to subrange type variables, or index expressions lie between two bounds, or that pointers are not textttnil, ... We present here a general algorithm allowing most of these certifications to be done at compile time.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} }
Henkin L, Monk J D, Tarski A
Cylindric Algebras: Part I Book
North-Holland, Amsterdam, 1971, ISBN: 978-0-7204-2043-2.
@book{HenkinMT71, title = {Cylindric Algebras: Part I}, author = {L. Henkin and J. D. Monk and A. Tarski}, isbn = {978-0-7204-2043-2}, year = {1971}, date = {1971-01-01}, publisher = {North-Holland}, address = {Amsterdam}, keywords = {}, pubstate = {published}, tppubtype = {book} }
Stoer J, Witzgall C
Convexity and Optimization in Finite Dimensions I Book
Springer-Verlag, Berlin, 1970.
@book{StoerW70, title = {Convexity and Optimization in Finite Dimensions I}, author = {J. Stoer and C. Witzgall}, year = {1970}, date = {1970-01-01}, publisher = {Springer-Verlag, Berlin}, keywords = {}, pubstate = {published}, tppubtype = {book} }
Chernikova N V
Algorithm for Discovering the Set of all Solutions of a Linear Programming Problem Journal Article
In: U.S.S.R. Computational Mathematics and Mathematical Physics, vol. 8, no. 6, pp. 282–293, 1968.
@article{Chernikova68, title = {Algorithm for Discovering the Set of all Solutions of a Linear Programming Problem}, author = {N. V. Chernikova}, year = {1968}, date = {1968-01-01}, journal = {U.S.S.R. Computational Mathematics and Mathematical Physics}, volume = {8}, number = {6}, pages = {282–293}, publisher = {MAIK NAUKA/Interperiodica Publishing, Moscow}, abstract = {In this paper two versions of a canonical algorithm for discovering all the optimal solutions of a linear programming problem with the condition of non-negativeness of the variables are presented: the first for the case of canonical notation, the second for the standard notation.}, keywords = {}, pubstate = {published}, tppubtype = {article} }
Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Inequalities Journal Article
In: U.S.S.R. Computational Mathematics and Mathematical Physics, vol. 5, no. 2, pp. 228–233, 1965.
@article{Chernikova65, title = {Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Inequalities}, author = {N. V. Chernikova}, year = {1965}, date = {1965-01-01}, journal = {U.S.S.R. Computational Mathematics and Mathematical Physics}, volume = {5}, number = {2}, pages = {228–233}, publisher = {MAIK NAUKA/Interperiodica Publishing, Moscow}, abstract = {The present note proposes a computational scheme for finding a general formula for the non-negative solutions of a system of linear inequalities analogous to the scheme described in citeChernikova64 for finding a general formula for the non-negative solutions of a system of linear equations.}, keywords = {}, pubstate = {published}, tppubtype = {article} }
Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Equations Journal Article
In: U.S.S.R. Computational Mathematics and Mathematical Physics, vol. 4, no. 4, pp. 151–158, 1964.
@article{Chernikova64, title = {Algorithm for Finding a General Formula for the Non-Negative Solutions of System of Linear Equations}, author = {N. V. Chernikova}, year = {1964}, date = {1964-01-01}, journal = {U.S.S.R. Computational Mathematics and Mathematical Physics}, volume = {4}, number = {4}, pages = {151–158}, publisher = {MAIK NAUKA/Interperiodica Publishing, Moscow}, keywords = {}, pubstate = {published}, tppubtype = {article} }
Dantzig G B
Linear Programming and Extensions Book
Princeton University Press, Princeton, NJ, 1963.
@book{Dantzig63, title = {Linear Programming and Extensions}, author = {G. B. Dantzig}, year = {1963}, date = {1963-01-01}, publisher = {Princeton University Press}, address = {Princeton, NJ}, keywords = {}, pubstate = {published}, tppubtype = {book} }
Kuhn H W
Solvability and Consistency for Linear Equations and Inequalities Journal Article
In: American Mathematical Monthly, vol. 63, pp. 217–232, 1956.
@article{Kuhn56, title = {Solvability and Consistency for Linear Equations and Inequalities}, author = {H. W. Kuhn}, year = {1956}, date = {1956-01-01}, journal = {American Mathematical Monthly}, volume = {63}, pages = {217–232}, keywords = {}, pubstate = {published}, tppubtype = {article} }
Motzkin T S, Raiffa H, Thompson G L, Thrall R M
The Double Description Method Book Section
In: Kuhn H W, Tucker A W (Ed.): Contributions to the Theory of Games – Volume II, no. 28, pp. 51–73, Princeton University Press, Princeton, New Jersey, 1953.
@incollection{MotzkinRTT53, title = {The Double Description Method}, author = {T. S. Motzkin and H. Raiffa and G. L. Thompson and R. M. Thrall}, editor = {H. W. Kuhn and A. W. Tucker}, year = {1953}, date = {1953-01-01}, booktitle = {Contributions to the Theory of Games – Volume II}, number = {28}, pages = {51–73}, publisher = {Princeton University Press}, address = {Princeton, New Jersey}, series = {Annals of Mathematics Studies}, abstract = {The purpose of this paper is to present a computational method for the determination of the value and of all solutions of a two-person zero-sum game with a finite number of pure strategies, and for the solution of general finite systems of linear inequalities and corresponding maximization problems.}, keywords = {}, pubstate = {published}, tppubtype = {incollection} }
