\"Uberpr\"ufung von Integrit\"atsbedingungen in Deduktiven Datenbanken

• URL: http://arxiv.org/abs/2304.09944v1
• Date: Tue, 21 Mar 2023 21:07:15 GMT
• Title: \"Uberpr\"ufung von Integrit\"atsbedingungen in Deduktiven Datenbanken
• Authors: Stefan Decker
• Abstract summary: Integrity violations can be interpreted as special operations on proofs of integrity constraints. We define a proof tree as a special data structure and demonstrate the implication of the existence of an SLDNF proof through such a tree. We determine a minimal set of conditions that specify when a change in the knowledge base affects the validity of an integrity constraint.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Advancements in computer science and AI lead to the development of larger, more complex knowledge bases. These are susceptible to contradictions, particularly when multiple experts are involved. To ensure integrity during changes, procedures are needed. This work addresses the problem from a logical programming perspective. Integrity violations can be interpreted as special operations on proofs of integrity constraints, with SLDNF proofs being the focus. We define a proof tree as a special data structure and demonstrate the implication of the existence of an SLDNF proof through such a tree. Proof trees are more convenient than SLDNF trees and allow set-oriented considerations of proofs. They also present the proof structure more clearly, enabling further applications. Using this structure, we determine a minimal set of conditions that specify when a change in the knowledge base affects the validity of an integrity constraint. Additionally, this approach allows for the reuse of large parts of the old proof when searching for a new one, which reduces the effort compared to previous approaches.

Related papers

• Structural Entropy Guided Probabilistic Coding [52.01765333755793]
  We propose a novel structural entropy-guided probabilistic coding model, named SEPC. We incorporate the relationship between latent variables into the optimization by proposing a structural entropy regularization loss. Experimental results across 12 natural language understanding tasks, including both classification and regression tasks, demonstrate the superior performance of SEPC.
  arXiv  Detail & Related papers  (2024-12-12T00:37:53Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
  arXiv  Detail & Related papers  (2024-12-11T19:17:28Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure. Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
  arXiv  Detail & Related papers  (2024-10-17T12:48:14Z)
• Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
  We propose a novel proof aggregation approach based on OR logic for Merkle tree inclusion proofs. We achieve a proof size independent of the number of leaves in the tree, and verification can be performed using any single valid leaf hash. The proposed techniques have the potential to significantly enhance the scalability, efficiency, and flexibility of zero-knowledge proof systems.
  arXiv  Detail & Related papers  (2024-05-13T17:15:38Z)
• Enhancing Systematic Decompositional Natural Language Inference Using Informal Logic [51.967603572656266]
  We introduce a consistent and theoretically grounded approach to annotating decompositional entailment. We find that our new dataset, RDTE, has a substantially higher internal consistency (+9%) than prior decompositional entailment datasets. We also find that training an RDTE-oriented entailment classifier via knowledge distillation and employing it in an entailment tree reasoning engine significantly improves both accuracy and proof quality.
  arXiv  Detail & Related papers  (2024-02-22T18:55:17Z)
• Latent Hierarchical Causal Structure Discovery with Rank Constraints [19.61598654735681]
  We consider a challenging scenario for causal structure identification, where some variables are latent and they form a hierarchical graph structure. We propose an estimation procedure that can efficiently locate latent variables, determine their cardinalities, and identify the latent hierarchical structure.
  arXiv  Detail & Related papers  (2022-10-01T03:27:54Z)
• Interpretable Proof Generation via Iterative Backward Reasoning [37.03964644070573]
  We present IBR, an Iterative Backward Reasoning model to solve the proof generation tasks on rule-based Question Answering (QA) We handle the limitations of existed works in two folds: 1) enhance the interpretability of reasoning procedures with detailed tracking, by predicting nodes and edges in the proof path iteratively backward from the question; 2) promote the efficiency and accuracy via reasoning on the elaborate representations of nodes and history paths, without any intermediate texts that may introduce external noise during proof generation.
  arXiv  Detail & Related papers  (2022-05-22T02:44:14Z)
• Causal de Finetti: On the Identification of Invariant Causal Structure in Exchangeable Data [45.389985793060674]
  Constraint-based causal discovery methods leverage conditional independence tests to infer causal relationships in a wide variety of applications. We show that exchangeable data contains richer conditional independence structure than i.i.d.$ $ data, and show how the richer structure can be leveraged for causal discovery.
  arXiv  Detail & Related papers  (2022-03-29T17:10:39Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)
• On $\ell_p$-norm Robustness of Ensemble Stumps and Trees [83.81523991945018]
  We develop an efficient programming based algorithm for sound verification of ensemble stumps. We demonstrate the first certified defense method for training ensemble stumps and trees with respect to $ell_p$ norm perturbations.
  arXiv  Detail & Related papers  (2020-08-20T03:42:40Z)
• CSNE: Conditional Signed Network Embedding [77.54225346953069]
  Signed networks encode positive and negative relations between entities such as friend/foe or trust/distrust. Existing embedding methods for sign prediction generally enforce different notions of status or balance theories in their optimization function. We introduce conditional signed network embedding (CSNE) Our probabilistic approach models structural information about the signs in the network separately from fine-grained detail.
  arXiv  Detail & Related papers  (2020-05-19T19:14:52Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.