Similarity-Based Equational Inference in Physics
Automating the derivation of published results is a challenge, in part due to the informal use of mathematics by physicists, compared to that of mathematicians. Following demand, we describe a method for converting informal hand-written derivations into datasets, and present an example dataset crafted from a contemporary result in condensed matter. We define an equation reconstruction task completed by rederiving an unknown intermediate equation posed as a state, taken from three consecutive equational states within a derivation. Derivation automation is achieved by applying string-based CAS-reliant actions to states, which mimic mathematical operations and induce state transitions. We implement a symbolic similarity-based heuristic search to solve the equation reconstruction task as an early step towards multi-hop equational inference in physics.
Code (1)
Tasks
Heuristic SearchSimilar Papers 제목 키워드 기반
E-Generalization Using Grammars
We extend the notion of anti-unification to cover equational theories and present a method based on regular tree grammars to compute a finite representation of E-generalization sets. We present a framework to combine Ind…
Inductive logic programmingImplementing Anti-Unification Modulo Equational Theory
We present an implementation of E-anti-unification as defined in Heinz (1995), where tree-grammar descriptions of equivalence classes of terms are used to compute generalizations modulo equational theories. We discuss se…
LEMMAOn Incorrectness Logic and Kleene Algebra with Top and Tests
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas.…
Fuzzy inequational logic
We present a logic for reasoning about graded inequalities which generalizes the ordinary inequational logic used in universal algebra. The logic deals with atomic predicate formulas of the form of inequalities between t…
NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
We present a new dependent type system, NM-DEKL$^3_\infty$ (Non-Monotone Dependent Knowledge-Enhanced Logic), for formalising evolving knowledge in dynamic environments. The system uses a three-layer architecture separat…