首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到10条相似文献,搜索用时 93 毫秒
1.
We investigate the complexity of deciding whether for minimal unsatisfiable formulas F and H there exists a variable renaming, a literal renaming or a homomorphism such that (F) = H. A variable renaming is a permutation of variables. A literal renaming is a permutation of variables which additionally replaces some of the variables by its complements. A homomorphism can be considered as a literal renaming which can map different literals to one literal.  相似文献   

2.
We formalize natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgment we model is of the form d[:], stating that d is a proof term of formula under hypotheses it can be viewed as a typing relation by the Curry–Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.  相似文献   

3.
We give an O(k · n2) fixed parameter tractable algorithm for the 1-Sided Crossing Minimization. The constant in the running time is the golden ratio = (1+5)/2 1.618. The constant k is the parameter of the problem: the number of allowed edge crossings.  相似文献   

4.
A variotherm mold for micro metal injection molding   总被引:4,自引:1,他引:3  
In this paper, a variotherm mold was designed and fabricated for the production of 316L stainless steel microstructures by micro metal injection molding (MIM). The variotherm mold incorporated a rapid heating/cooling system, vacuum unit, hot sprue and cavity pressure transducer. The design of the variotherm mold and the process cycle of MIM using the variotherm mold were described. Experiments were conducted to evaluate the molded microstructures produced using variotherm mold and conventional mold. The experiments showed that microstructures of higher aspect ratio such as 60 m × height 191 m and 40 m × height 174 m microstructures could be injection molded with complete filling and demolded successfully using the variotherm mold. Molded microstructures with dimensions of 60 m × height 191 m were successfully debound and sintered without visual defects.  相似文献   

5.
Our starting point is a definition of conditional event EH which differs from many seemingly similar ones adopted in the relevant literature since 1935, starting with de Finetti. In fact, if we do not assign the same third value u (undetermined) to all conditional events, but make it depend on EH, it turns out that this function t(EH) can be taken as a general conditional uncertainty measure, and we get (through a suitable – in a sense, compulsory – choice of the relevant operations among conditional events) the natural axioms for many different (besides probability) conditional measures.  相似文献   

6.
Let H be a separable Hilbert space. We consider the manifold M consisting of density operators on H such that p is of trace class for some p (0, 1). We say M is nearby if there exists C > 1 such that C –1C. We show that the space of nearby points to can be furnished with the two flat connections known as the (±)-affine structures, which are dual relative to the BKM metric. We furnish M with a norm making it into a Banach manifold.  相似文献   

7.
We show that a mixed state = mnamn|mn| can be realized by an ensemble of pure states {pk, |k} where . Employing this form, we discuss the relative entropy of entanglement of Schmidt correlated states. Also, we calculate the distillable entanglement of a class of mixed states. PACS: 03.67.-a; 03.65.Bz; 03.65.Ud  相似文献   

8.
This paper describes a machine for reducing a -formula (explicitly given or implicitly by a system of recursive equations) to principal --normal form, with particular attention to the memory structures needed for the purpose, and with some important features: (1) any kind of collision is permitted; (2) the processing of subformulas which will be thrown away [e.g., ((xy)x) in ((yz)(xy)x)] is avoided; (3) there is no need to introduce any fixed point operator like , etc. The machine structure entails: (1) some store to memorize as side-effects assignment statements with the r.h.s. of a given shape. (2) a number of stacks, one for every in the initial formula, partitioned naturally in classes (chains). These stacks admit as entries only words representing variables and they are peculiar in that the operations admitted on the top arewriting anderasing and the operations admitted on the pseudo-top arereading,read-protecting, andresetting readability (the last two operations are chain operations). This structure is critically motivated. (3) A workstack. (4) A pointerstack. The computation runs through four phases: -generation, -run, -generation, -run. Every generation- (run-) phase is rather recognition- (transformation-) oriented, but we found it more stimulating to emphasize technical similarities rather than methodological differences. Every phase is described and four examples are extensively developed.  相似文献   

9.
Let F=C 1C m be a Boolean formula in conjunctive normal form over a set V of n propositional variables, s.t. each clause C i contains at most three literals l over V. Solving the problem exact 3-satisfiability (X3SAT) for F means to decide whether there is a truth assignment setting exactly one literal in each clause of F to true (1). As is well known X3SAT is NP-complete [6]. By exploiting a perfect matching reduction we prove that X3SAT is deterministically decidable in time O(20.18674n ). Thereby we improve a result in [2,3] stating X3SATO(20.2072n ) and a bound of O(20.200002n ) for the corresponding enumeration problem #X3SAT stated in a preprint [1]. After that by a more involved deterministic case analysis we are able to show that X3SATO(20.16254n ).  相似文献   

10.
Let K be a permutation group acting on binary vectors of length n and F K be a code of length 2 n consisting of all binary functions with nontrivial inertia group in K. We obtain upper and lower bounds on the covering radii of F K , where K are certain subgroups of the affine permutation group GA n . We also obtain estimates for distances between F K and almost all functions in n variables as n . We prove the existence of functions with the trivial inertia group in GA n for all n 7. An upper bound for the asymmetry of a k-uniform hypergraph is obtained.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号