Zobrazeno 1 - 10
of 133
pro vyhledávání: '"Weidenbach, Christoph"'
We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. The completeness proof of super
Externí odkaz:
http://arxiv.org/abs/2305.12926
Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existence of a model. We present an effective symbolic model construction for
Externí odkaz:
http://arxiv.org/abs/2305.05064
This paper presents an up-to-date and refined version of the SCL calculus for first-order logic without equality. The refinement mainly consists of the following two parts: First, we incorporate a stronger notion of regularity into SCL(FOL). Our regu
Externí odkaz:
http://arxiv.org/abs/2302.05954
Abduction in description logics finds extensions of a knowledge base to make it entail an observation. As such, it can be used to explain why the observation does not follow, to repair incomplete knowledge bases, and to provide possible explanations
Externí odkaz:
http://arxiv.org/abs/2205.08449
We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption
Externí odkaz:
http://arxiv.org/abs/2205.08297
Autor:
Bromberger, Martin, Dragoste, Irina, Faqeh, Rasha, Fetzer, Christof, González, Larry, Krötzsch, Markus, Marx, Maximilian, Murali, Harish K, Weidenbach, Christoph
In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation
Externí odkaz:
http://arxiv.org/abs/2201.09769
Autor:
Bromberger, Martin, Dragoste, Irina, Faqeh, Rasha, Fetzer, Christof, Krötzsch, Markus, Weidenbach, Christoph
The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR) clause sets with both universally and existentially quantified verification conditions (conjec
Externí odkaz:
http://arxiv.org/abs/2107.03189
We lift the SCL calculus for first-order logic without equality to the SCL(T) calculus for first-order logic without equality modulo a background theory. In a nutshell, the SCL(T) calculus describes a new way to guide hierarchic resolution inferences
Externí odkaz:
http://arxiv.org/abs/2003.04627
Autor:
Weidenbach, Christoph
Publikováno v:
EPTCS 311, 2019, pp. 5-10
While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fragments thereof. In particular, they can result in short proofs or mode
Externí odkaz:
http://arxiv.org/abs/1912.12966
A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of monadic, shallow,
Externí odkaz:
http://arxiv.org/abs/1905.03651