|
 REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
APSVALL, B., AND SHILOACH, Y A polynomial-time algorithm for solvmg systems of hnear equahtles with two variables per inequality Proc 20th Ann Symp on Foundations of Computer Science, San Juan, Puerto Rico, 1979, pp 205-217 Also to appear in SIAM J Comput
|
| |
2
|
BLEDSOE, W W Program correctness Memo ATP-14, MathemaUcs Dep, Umv of Texas, Austm, Texas, Jan 1974
|
| |
3
|
BLEOSOE, W W.The sup-mf method in Presburger arithmetic Memo ATP-18, Mathematics Dep, Univ. of Texas, Austm, Texas, Dec. 1974.
|
| |
4
|
BLEDSOE, W W A new method for provmg certain Presburger formulas Advance Papers, 4th Int Joint Conf on Artificial Intelligence, Tlbdts~, Russia, Sept. 1975, pp 15-21
|
| |
5
|
BLEDSOE, W W, BORER, R S, AND HENNEMAN, W H Computer proofs of limit theorems Artf lntell 3 (1972), 27-60
|
| |
6
|
BLEDSOE, W W., AND BRUELL, P A man-machme theorem-proving system Amf Intell 5 (1974), 51-72
|
| |
7
|
COOPER, D C. Programs for mechamcal program verlficauon In Machme Intelhgence 6, B Meltzer, Ed, American Elsevier, New York, 197 i, pp 43-59
|
| |
8
|
DANTZIG, G B Linear Programming and Extensions Princeton University Press, Princeton, N J, 1962
|
| |
9
|
DEUTCH, L P An interactive program verifier Ph D Dissertation, Umv of Cahfornla, Berkeley, Cahf., 1973
|
| |
10
|
ELSPAS, B., BOYER, R E, SHOSTAK, R, AND SPITZEN, J A venficauon system for JOVIAL/J3 programs Tech Rep 3756-1, Stanford Research Institute, Menlo Park, Cahf, Jan 1976.
|
| |
11
|
GOMORY, R E An algorithm for integer soluUons to linear programs Princeton IBM Math Res Report, Nov 1958 Also in Recent Advances m Mathematical Programming, R L Graves and P Wolfe, Eds, McGraw-Hill, N Y., 1963, pp 269-302
|
 |
12
|
|
| |
13
|
|
| |
14
|
JOHNSON, D B Finding all the elementary circuits of a directed graph SIAM J Comput 4 (1975), 77-84
|
| |
15
|
|
| |
16
|
KHACHIYAN, L.G A polynomial algorithm in linear programming. Dokl Akad Nauk SSSR Nov Ser 244, 5 (1979), 1093-1096 {Eng trans in Soy Math Dokl 20, 1 (1979), 191-194}
|
| |
17
|
LEE, R D.An apphcatlon of mathematical logic to the integer linear programming problem Notre Dame J Formal Log:c XIH, 2 (April 1972)
|
| |
18
|
LITVINTCHOUK, S D, mqD PRATT, V R.A proof checker for dynamic logic 5th lnt Joint Conf on Artificial Intelligence, Boston, Mass, August 1977, pp 552-558
|
| |
19
|
MATETI, P., AND PRABHAKER, M On algorithms for enumerating all orcmts of a graph SlAM J Comput 5 (March 1976), 90-99
|
| |
20
|
PRATT, V R Two easy theories whose combination is hard. Tech. Rep, Massachusetts Institute of Technology, Cambridge, Mass., Sept 1977
|
| |
21
|
READ, R.C, AND TARJAN, R E. Bounds on backtrack algorithms for listing cycles, paths, and spanning trees. ERL Memo M 433, Electromcs Research Lab, Univ. of California, Berkeley, Calif, 1973.
|
| |
22
|
SHOSTAK, R. An effioent decision procedure for arithmetic with function symbols. Presented at 5th Int. joint Conf. on ArUficml Intelhgence, Cambridge, Mass., Aug 1977.
|
| |
23
|
|
| |
24
|
|
| |
25
|
SZWARCFITER, J.L, AND LAUER, P E Finding the elementary cycles of a d~rected graph in O(n + m) per cycle. Tech. Rep No. 60, Umv. of Newcastle upon Tyne, Newcastle upon Tyne, England, May 1974
|
| |
26
|
TARJAN, R. Enumeration of the elementary circuits of a directed graph SlAM J. Comput. 2, 3 (Sept. 1973), 211-216.
|
| |
27
|
WALDINGER, R J, AND LEVITT, K.N. Reasoning about programs. J. Art,f lntell. 5 (1974), 235-316.
|
CITED BY 34
|
|
|
|
|
Carolyn Habit Norton , Serge A. Plotkin , Éva Tardos, Using separation algorithms in fixed dimension, Proceedings of the first annual ACM-SIAM symposium on Discrete algorithms, p.377-387, January 22-24, 1990, San Francisco, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Allen Goldberg , T. C. Wang , David Zimmerman, Applications of feasible path analysis to program testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.80-94, August 17-19, 1994, Seattle, Washington, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
G S Lueker , N Megiddo , V Ramachandran, Linear programming with two variables per inequality in poly-log time, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.196-205, May 28-30, 1986, Berkeley, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lina Khatib , Paul Morris , Robert Morris , Francesca Rossi , Alessandro Sperduti , K. Brent Venable, Solving and learning a tractable class of soft temporal constraints: Theoretical and experimental results, AI Communications, v.20 n.3, p.181-209, August 2007
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
G.1