\"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
• 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

• The Equivalence Theorem: First-Class Relationships for Structurally Complete Database Systems [0.0]
  We prove The Equivalence Theorem: structurally complete knowledge representation requires exactly four entailing capabilities.<n>We show an Attributed Temporal Causal Hypergraph framework satisfying all four conditions simultaneously.<n>We derive solutions to classical AI problems: the Frame Problem, conflict resolution, and common sense reasoning.
  arXiv  Detail & Related papers  (2026-03-13T21:21:21Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• Deriving Character Logic from Storyline as Codified Decision Trees [67.01182739162142]
  Role-playing (RP) agents rely on behavioral profiles to act consistently across diverse narrative contexts.<n>We propose Codified Decision Trees (CDT), a data-driven framework that induces an executable and interpretable decision structure from large-scale narrative data.
  arXiv  Detail & Related papers  (2026-01-15T05:12:43Z)
• Illusions of Confidence? Diagnosing LLM Truthfulness via Neighborhood Consistency [78.91846841708586]
  We show that even facts answered with perfect self-consistency can rapidly collapse under mild contextual interference.<n>We propose Neighbor-Consistency Belief (NCB), a structural measure of belief that evaluates response coherence across a conceptual neighborhood.<n>We also present Structure-Aware Training (SAT), which optimize context-invariant belief structure and reduces long-tail knowledge brittleness by approximately 30%.
  arXiv  Detail & Related papers  (2026-01-09T16:23:21Z)
• Gödel's Poetry [0.0]
  We introduce a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation.<n>We achieve a 90.4% pass rate on miniF2F without decomposition.<n>A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities.
  arXiv  Detail & Related papers  (2025-12-16T10:00:01Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  We conduct a user study involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages.<n>Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process.<n>We translate these findings into concrete design guidance for AI proof assistants.
  arXiv  Detail & Related papers  (2025-08-01T22:16:30Z)
• 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)
• A simple geometric proof for the benefit of depth in ReLU networks [57.815699322370826]
  We present a simple proof for the benefit of depth in multi-layer feedforward network with rectified activation ("depth separation") We present a concrete neural network with linear depth (in $m$) and small constant width ($leq 4$) that classifies the problem with zero error.
  arXiv  Detail & Related papers  (2021-01-18T15:40:27Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)
• 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.