A Unified Approach to Theory Reasoning

Keywords

Completeness (order theory), Inference, Literal (mathematical logic), Automated reasoning, Domain theory

References

• Automated theorem proving: a logical basisDonald Loveland — 1978
• Consolution and its Relation with ResolutionElmar Eder — 1991
• A Model Elimination Calculus with Built-in TheoriesPeter Baumgartner — 1992
• Theorem Proving Using Rigid E-Unification Equational MatingsJean Gallier, Stan Raatz, Wayne Snyder — 1987
• Deduction systems in artificial intelligenceMarco Antonio Arranz Martín — 1994
• Consolution as a Framework for Comparing CalculiPeter Baumgartner, Ulrich Furbach — 1993
• A Technique for Establishing Completeness Results in Theorem Proving with EqualityGerald E. Peterson — 1983
• Proof theory for general unificationWayne Snyder — 1991
• Logic for Computer Science: Foundations of Automatic Theorem ProvingJean Gallier — 1985
• Formal Logic: Its Scope and LimitsRichard C. Jeffrey — 1981
• Symbolic logic and mechanical theorem provingChin-Liang Chang, Richard C. T. Lee — 1973
• A Many-Sorted Calculus Based on Resolution and ParamodulationChristoph Walther — 1982
• Solving Equations in Abstract Algebras: A Rule-Based Survey of UnificationJean-Pierre Jouannaud, Claude Kirchner — 1991
• Constraint Satisfaction Problems: An OverviewPedro Meseguer — 1989
• Adding Equality to Semantic TableauxBernhard Beckert — 2006
• Krypton: A Functional Approach to Knowledge RepresentationBrachman, Fikes, Levesque — 1983
• Horn equational theories and paramodulationUlrich Furbach, Steffen H�lldobler, Joachim Schreiber — 1989
• Multimodal Logic Programming Using Equational and Order-Sorted LogicFrançoise Debart, Patrice Enjalbert, Madeleine Lescot — 1992
• Theory Links: Applications to Automated Theorem ProvingNeil V. Murray, Erik Rosenthal — 1987
• Constraint satisfaction in logic programmingPascal Van Hentenryck — 1989

Cited by

• A comprehensive combination frameworkSilvio Ghilardi, Enrica Nicolini, Daniele Zucchelli — 2008
• Axiomatic Constraint Systems for Proof Search Modulo TheoriesDamien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand — 2014
• Combination Methods for Verification ProblemsDaniele Zucchelli — 2008
• Extension into trees of first order theoriesKhalil Djelloul, Thi-Bich-Hanh Dao — 2006
• Extension of First-Order Theories into TreesKhalil Djelloul, T. Dao — 2006
• Noetherianity and Combination ProblemsS. Ghilardi, Enrica Nicolini, Silvio Ranise — 2007
• A Grand Challenge for Computing Research : A Mathematical AssistantT. Walsh
• ombination methods for software verification. (Méthodes de combinaison pour la vérification de logiciels)D. Zucchelli — 2008

Related papers

• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear LogicAdams, Robin, Jacobs, Bart — 2017
• A Framework for Single-Condition Approximate ReasoningRongyu He, Chaowen Chang — 2006
• Probabilistic logic under coherence: complexity and algorithmsVeronica Biazzo, Angelo Gilio, Thomas Lukasiewicz — 2005
• Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of peopleAlexander Sobol, Е. И. Козлова, Yu. A. Chernyavsky — 2021
• Plausible Reasoning and the Theory of EvidenceGraham Reynolds, D. Strahman, Nancy Bonar Lehrer — 1986