Extractive methods for machine reading comprehension (MRC) tasks have achieved comparable or better accuracy than human performance on benchmark data sets. However, such models are not as successful when adapted to complex domains such as health care. One of the main reasons is that the context that the MRC model needs to process when operating in a complex domain can be much larger compared with an average open-domain context. This causes the MRC model to make less accurate and slower predictions. A potential solution to this problem is to reduce the input context of the MRC model by extracting only the necessary parts from the original context.
In this paper we propose a context-based approach to abstract theorem proving. The challenges stem from the need to identify an abstract level for theorem proving where (less important) information can be temporarily ignored so that a (plan for a) proof of the abstracted problem can be devised to guide the (re)construction of the object-level proof. Contextualization is realized by preserving the logical structures of the formulas of the original representation while pushing the less important subformulas, according to a relevance relation, into the hierarchical subcontexts. This representation allows the problem to be gradually unfolded during the proof search process by hierarchically exploring the subcontexts required to provide support for the hypotheses used in the proof plan. The underlying inference machinery is also equipped with an assertion application module which allows mathematical assertions such as axioms, definitions, theorems, and even global and local assumptions to be applied directly to a proof situation to obtain their logical consequences (from the applied proof situation) and fill in the gaps opened up by an abstract-level proof step. This guarantees that our achievement is two-fold: on the one hand, we are able to carry out effective techniques to search for and construct proofs for a problem; on the other hand, the constructed proof is readily at a sufficiently high level of abstraction so that it can be communicated directly to human mathematicians without undergoing a proof transformation process as required by most machine-generated proofs.
Route finding issues have always been a significant research focus in intelligence transportation system. Many solution models have been proposed in the previous work and analyzed in detail. Successive link travel time correlation has been identified to play an important role in these models to realistically reflect the property of traffic flows. In this paper, we establish a framework to find the best route in a stochastic time-dependent network by considering link travel time indeterminacy and correlation between adjacent links with real time information. We provide explicit mathematical formulations to update the outing link travel time distributions according to the real time information and help the travelers to find the best route to their destination. A simple illustrative example is shown to demonstrate the effectiveness and advantages of the proposed method.
In this paper, we introduce an alternative approach to reasoning about action.The approach provides a solution to the frame and the ramification problem in a uniform manner.The approach involves keeping a (syntax-based) model of the world that is updated when actions are performed.Our approach is similar to the STRIPS system in which formulas are deleted and added as effects of an action.The presented framework however does not suffer from STRIPS' limitations in expressivity.
'/%3e%3c/defs%3e%3cpath fill='%23012169' d='M0 0h10080v5040H0z'/%3e%3cpath stroke='%23fff' stroke-width='.6' d='m0 0 6 3m0-3L0 3' clip-path='url(%23b)' transform='scale(840)'/%3e%3cpath stroke='%23e4002b' stroke-width='.4' d='m0 0 6 3m0-3L0 3' clip-path='url(%23c)' transform='scale(840)'/%3e%3cpath stroke='%23fff' stroke-width='840' d='M2520 0v2520M0 1260h5040'/%3e%3cpath stroke='%23e4002b' stroke-width='504' d='M2520 0v2520M0 1260h5040'/%3e%3cg fill='%23fff'%3e%3cuse xlink:href='%23d' x='2520' y='3780'/%3e%3cuse xlink:href='%23a' x='7560' y='4200'/%3e%3cuse xlink:href='%23a' x='6300' y='2205'/%3e%3cuse xlink:href='%23a' x='7560' y='840'/%3e%3cuse xlink:href='%23a' x='8680' y='1869'/%3e%3cuse xlink:href='%23e' x='8064' y='2730'/%3e%3c/g%3e%3c/svg%3e)
'/%3e%3cuse xlink:href='%23a' transform='rotate(23.036 .093 25.536)'/%3e%3cuse xlink:href='%23a' transform='rotate(45.87 1.273 16.18)'/%3e%3cuse xlink:href='%23a' transform='rotate(69.945 .996 12.078)'/%3e%3cuse xlink:href='%23a' transform='rotate(20.66 -19.689 31.932)'/%3e%3c/svg%3e)
