Nebulizer
发表于 2025-3-23 10:14:30
Instructing Equational Set-Reasoning with Otter within the ground formalism .developed by Tarski and Givant. On top of a kernel axiomatization of map algebra we develop a layered formalization of basic set-theoretical concepts. A first-order theorem prover is exploited to obtain automated certification and validation of this layered architecture
歪曲道理
发表于 2025-3-23 15:37:55
http://reply.papertrans.cn/17/1664/166319/166319_12.png
横条
发表于 2025-3-23 21:21:42
Ordered Resolution vs. Connection Graph resolutionxpected unrestricted connection graph (cg) resolution to be strongly complete until Eisinger proved that it was not. In this paper, ordered resolution is shown to be a special case of cg-resolution, and that relationship is used to prove that ordered cg-resolution is strongly complete. On the other
Emasculate
发表于 2025-3-24 00:38:01
A Model-Based Completeness Proof of Extended Narrowing and Resolutioncontext of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for findi
允许
发表于 2025-3-24 02:53:11
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equalitycontain at most two variables. This paper shows how resolution theorem-proving techniques can be used to provide an algorithm for deciding whether any given formula in .is satisfiable. Previous resolution-based techniques could deal only with the equality-free subset .of the two-variable fragment.
增强
发表于 2025-3-24 06:52:00
Superposition and Chaining for Totally Ordered Divisible Abelian Groupsprevious superposition or chaining calculi for divisible torsion-free abelian groups and dense total orderings without endpoints. As its predecessors, it is refutationally complete and requires neither explicit inferences with the theory axioms nor variable overlaps. It offers thus an efficient way
Classify
发表于 2025-3-24 14:28:00
Context Treess where terms are seen as strings and common prefixes are shared, and substitution trees, where terms keep their tree structure and all common contexts can be shared. Here we describe a new indexing data structure, called context trees, where, by means of a limited kind of context variables, also co
Coma704
发表于 2025-3-24 15:32:14
On the Evaluation of Indexing Techniques for Theorem Provinglled the .), identify the subset . of . that consists of the terms . such that . holds. Terms in M will be called the .. Typical retrieval conditions used in first-order theorem proving are matching, generalization, unifiability, and syntactic equality. Such a retrieval of candidate terms in theorem
mastopexy
发表于 2025-3-24 19:26:52
The Description Logic ,,, Extended with Concrete Domains: A Practically Motivated Approach this operator. This results in a limited expressivity w.r.t. concrete domains but is required to ensure the decidability of the language. We show that the results can be exploited for building practical description logic systems for solving e.g. configuration problems.
Gyrate
发表于 2025-3-24 23:10:45
NExpTime-Complete Description Logics with Concrete DomainsTBoxes, inverse roles, and a role-forming concrete domain constructor—that make reasoning NExpTime-hard. As a corresponding upper bound, we show that reasoning with all three extensions . is in NExpTime.