排序方式: 共有39条查询结果,搜索用时 31 毫秒
11.
Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo. 相似文献
12.
In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification
and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued
Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without
distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix,
incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy
logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which
correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi
of ordinary, two-valued sequents.
Presented by Yaroslav Shramko and Heinrich Wansing 相似文献
13.
The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi. 相似文献
14.
15.
Cut-free double sequent calculus for S5 总被引:2,自引:0,他引:2
16.
17.
18.
Journal of Philosophical Logic - Our aim is to express in exact terms the old idea of solving problems by pure questioning. We consider the problem of derivability: “Is A derivable from... 相似文献
19.
Norihiro Kamide 《Studia Logica》2005,80(2-3):265-289
A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based
on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or
re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical
logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed
sequent calculi including CLS (a conservative extension of CL) and CLScw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect
to phase semantics, for SLK (a conservative extension and fragment of LK and CLScw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw,
respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi
into LK, S4 and CL. 相似文献
20.
We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination.
Our conditions are formulated both syntactically and semantically. 相似文献