Tag #horn clause
50 papers:
ESOP-2019-BasoldKL #induction #proving #recursion- Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses (HB, EK, YL), pp. 783–813.
POPL-2018-BurnOR #higher-order #verification- Higher-order constrained horn clauses for verification (TCB, CHLO, SJR), p. 28.
SAS-2017-Albarghouthi #probability #verification- Probabilistic Horn Clause Verification (AA), pp. 1–22.
- SAS-2017-BakhirkinM #abstract interpretation
- Combining Forward and Backward Abstract Interpretation of Horn Clauses (AB, DM), pp. 23–45.
CAV-2017-UnnoTS #automation #induction- Automating Induction for Solving Horn Clauses (HU0, ST, HS), pp. 571–591.
LOPSTR-2016-AngelisFMPP #process #using #verification- Verification of Time-Aware Business Processes Using Constrained Horn Clauses (EDA, FF, MCM, AP, MP), pp. 38–55.
- SAS-2016-AngelisFPP #relational #verification
- Relational Verification Through Horn Clause Transformation (EDA, FF, AP, MP), pp. 147–169.
- SAS-2016-MonniauxG #array #source code
- Cell Morphing: From Array Programs to Array-Free Horn Clauses (DM, LG), pp. 361–382.
- CAV-2016-KafleGM #abstract interpretation #automaton #finite #named #using #verification
- Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata (BK, JPG, JFM), pp. 261–268.
PEPM-2015-KafleG #constraints #verification- Constraint Specialisation in Horn Clause Verification (BK, JPG), pp. 85–90.
TACAS-2015-UnnoT #recursion- Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling (HU, TT), pp. 149–163.
ICLP-J-2015-AngelisFPP #correctness #imperative #proving #source code- Proving correctness of imperative programs by linearizing constrained Horn clauses (EDA, FF, AP, MP), pp. 635–650.
- ICLP-J-2015-GangeNSSS #program analysis #program transformation #representation
- Horn clauses as an intermediate representation for program analysis and transformation (GG, JAN, PS, HS, PJS), pp. 526–542.
VMCAI-2015-KafleG #refinement #verification- Tree Automata-Based Refinement with Application to Horn Clause Verification (BK, JPG), pp. 209–226.
- SAS-2013-BjornerMR #on the #quantifier
- On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.
- CAV-2013-BeyenePR #quantifier
- Solving Existentially Quantified Horn Clauses (TAB, CP, AR), pp. 869–882.
- ICLP-J-2013-MazuranSZ #datalog #declarative
- A declarative extension of horn clauses, and its significance for datalog and its applications (MM, ES, CZ), pp. 609–623.
- TACAS-2012-GrebenshchikovGLPR #contest #verification
- HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.
CADE-2011-Horbach #set- Predicate Completion for non-Horn Clause Sets (MH), pp. 315–330.
KR-2010-DelgrandeW #set- Horn Clause Contraction Functions: Belief Set and Belief Base Approaches (JPD, RW).
- KR-2008-Delgrande
- Horn Clause Belief Change: Contraction Functions (JPD), pp. 156–165.
- ESOP-2008-NielsenNN
- Iterative Specialisation of Horn Clauses (CRN, FN, HRN), pp. 131–145.
PPDP-2006-Miller #analysis #source code- Collection analysis for Horn clause programs (DM), pp. 179–188.
- CADE-2005-VermaSS #complexity #equation #on the
- On the Complexity of Equational Horn Clauses (KNV, HS, TS), pp. 337–352.
- ICLP-2005-Ray #logic #query
- The Need for Ancestor Resolution When Answering Queries in Horn Clause Logic (OR), pp. 410–411.
- LOPSTR-2003-WangG #continuation #semantics
- Continuation Semantics as Horn Clauses (QW, GG), pp. 176–177.
- SAS-2002-NielsonNS #normalisation
- Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi (FN, HRN, HS), pp. 20–35.
ICML-1996-JappyNG #learning #robust #source code- Negative Robust Learning Results from Horn Clause Programs (PJ, RN, OG), pp. 258–265.
- LOPSTR-1995-ParkesW #induction #logic programming #synthesis
- Logic Program Synthesis by Induction over Horn Clauses (AJP, GAW), p. 170.
- ICLP-1995-DegtyarevV #similarity
- A New Procedural Interpretation of Horn Clauses with Equality (AD, AV), pp. 565–579.
CSL-1993-Marcinkowski #decidability #set- A Horn Clause that Implies and Undecidable Set of Horn Clauses (JM), pp. 223–237.
- ILPS-1993-DevienneLR #decidability #problem #recursion
- The Emptiness Problem of One Binary Recursive Horn Clause is Undecidable (PD, PL, JCR), pp. 250–265.
ICALP-1991-Dershowitz #set- Cononical Sets of Horn Clauses (ND), pp. 267–278.
ICSE-1990-GanzingerS #composition #order #specification- System Support for Modular Order-Sorted Horn Clause Specifications (HG, RS), pp. 150–159.
- CLP-1990-SchreyeVB90 #detection #graph #query #strict #using
- A Practical Technique for Detecting Non-terminating Queries for a Restricted Class of Horn Clauses, Using Directed, Weighted Graphs (DDS, KV, MB), pp. 649–663.
CCIPL-1989-Hanus #polymorphism #semantics #source code- Horn Clause Programs with Polymorphic Types: Semantics and Resolution (MH), pp. 225–240.
LICS-1989-BoseCLM #named #parallel #proving #theorem proving- PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
VLDB-1988-KrishnamurthyN #towards- Towards a Real Horn Clause Language (RK, SAN), pp. 252–263.
- ALP-1988-LiuL #fuzzy #reasoning
- Fuzzy Reasoning Based on F-Horn Clause Rules (DL, DL), pp. 214–222.
- CADE-1988-AllenBCM #named #parallel #proving #theorem proving
- PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
- CADE-1988-ChiH #query #recursion
- Recursive Query Answering with Non-Horn Clauses (SC, LJH), pp. 294–312.
- JICSCP-1988-Nystrom88
- Control Structures for Guarded Horn Clauses (SON), pp. 1351–1370.
PODS-1987-RamakrishnanBS #infinity #recursion #safety- Safety of Recursive Horn Clauses With Infinite Relations (RR, FB, AS), pp. 328–339.
- CAAP-1987-NavarroO #correctness #proving #specification
- Parameterized Horn Clause Specifications: Proof Theory and Correctness (MN, FO), pp. 202–216.
- CSL-1987-KarpinskiBS #complexity #on the #quantifier
- On the Computational Complexity of Quantified Horn Clauses (MK, HKB, PHS), pp. 129–137.
- ICLP-1987-ShmueliN87 #set #source code
- Set Grouping and Layering in Horn Clause Programs (OS, SAN), pp. 152–177.
- SLP-1986-GallierR86 #similarity
- SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification (JHG, SR), pp. 168–179.
- PODS-1982-ChandraH #fixpoint #query
- Horn Clauses and the Fixpoint Query Hierarchy (AKC, DH), pp. 158–163.
- ILPC-1982-Monteiro82 #concurrent #logic #specification
- A Horn Clause-like Logic for Specifying Concurrency (LM), pp. 1–8.
STOC-1980-Fagin #database #dependence- Horn Clauses and Database Dependencies (RF), pp. 123–134.
