An official website of the United States government
Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an “effective simulation,” which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution.
more »
« less
This content will become publicly available on March 1, 2026
Three-Dimensional Object Detection and High-Resolution Traffic Parameter Extraction Using Low-Resolution LiDAR Data
- Award ID(s):
- 2045786
- PAR ID:
- 10574275
- Publisher / Repository:
- ASCE LIBRARY
- Date Published:
- Journal Name:
- Journal of Transportation Engineering, Part A: Systems
- Volume:
- 151
- Issue:
- 3
- ISSN:
- 2473-2907
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
