Stem horn$ (all stems)

106 papers:

TACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification

SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.

TACAS-2015-UnnoT #horn clause #recursion

Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling (HU, TT), pp. 149–163.

PEPM-2015-KafleG #constraints #horn clause #verification

Constraint Specialisation in Horn Clause Verification (BK, JPG), pp. 85–90.

SAS-2015-HashimotoU #constraints #optimisation #refinement #type inference

Refinement Type Inference via Horn Constraint Optimization (KH, HU), pp. 199–216.

SAC-2015-GayathriK #rdf #rule-based

Horn-rule based compression technique for RDF data (VG, PSK), pp. 396–401.

CAV-2015-GurfinkelKKN #framework #verification

The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.

ICLP-J-2015-AngelisFPP #correctness #horn clause #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 #horn clause #program analysis #program transformation #representation

Horn clauses as an intermediate representation for program analysis and transformation (GG, JAN, PS, HS, PJS), pp. 526–542.

SAT-2015-ArifMM #axiom #performance

Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing (MFA, CM, JMS), pp. 324–342.

SAT-2015-MenciaPM #bound #satisfiability

SAT-Based Horn Least Upper Bounds (CM, AP, JMS), pp. 423–433.

VMCAI-2015-KafleG #horn clause #refinement #verification

Tree Automata-Based Refinement with Application to Horn Clause Verification (BK, JPG), pp. 209–226.

KR-2014-GarciaLS #finite #logic #reasoning

Finite Model Reasoning in Horn Description Logics (YAIG, CL, TS).

SAS-2013-BjornerMR #horn clause #on the #quantifier

On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.

SAC-2013-BanerjeeSS #detection #monitoring #using

Participatory sensing based traffic condition monitoring using horn detection (RB, AS, AS), pp. 567–569.

CAV-2013-BeyenePR #horn clause #quantifier

Solving Existentially Quantified Horn Clauses (TAB, CP, AR), pp. 869–882.

CAV-2013-RummerHK #verification

Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.

ICLP-J-2013-MazuranSZ #datalog #declarative #horn clause

A declarative extension of horn clauses, and its significance for datalog and its applications (MM, ES, CZ), pp. 609–623.

TACAS-2012-GrebenshchikovGLPR #contest #horn clause #verification

HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.

KR-2012-AdarichevaSST #complexity

Horn Belief Contraction: Remainders, Envelopes and Complexity (KVA, RHS, BS, GT).

KR-2012-ZhuangP #modelling

Model Based Horn Contraction (ZQZ, MP).

CADE-2011-Horbach #horn clause #set

Predicate Completion for non-Horn Clause Sets (MH), pp. 315–330.

ICALP-v1-2010-BhattacharyaDMT #approximate #on the

On Approximate Horn Formula Minimization (AB, BD, DM, GT), pp. 438–450.

KR-2010-DelgrandeW #horn clause #set

Horn Clause Contraction Functions: Belief Set and Belief Base Approaches (JPD, RW).

KR-2010-OrtizRS #owl #reasoning #worst-case

Worst-Case Optimal Reasoning for the Horn-DL Fragments of OWL 1 and 2 (MO, SR, MS).

SAT-2010-BubeckB #quantifier

Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN (UB, HKB), pp. 58–70.

SAT-2010-NamasivayamT

Simple but Hard Mixed Horn Formulas (GN, MT), pp. 382–387.

CADE-2009-SebastianiV #analysis #axiom #encoding #lightweight #logic

Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis (RS, MV), pp. 84–99.

SAT-2009-PorschenSS #aspect-oriented #on the

On Some Aspects of Mixed Horn Formulas (SP, TS, ES), pp. 86–100.

ESOP-2008-NielsenNN #horn clause

Iterative Specialisation of Horn Clauses (CRN, FN, HRN), pp. 131–145.

KR-2008-Delgrande #horn clause

Horn Clause Belief Change: Contraction Functions (JPD), pp. 156–165.

SEKE-2008-LiuLZL #logic #protocol #security

Supremum of Agent Number Needed in Analyzing Security Protocols Based on Horn Logic (FL, ZL, TZ, ML), pp. 795–801.

SAT-2008-KottlerKS

Computation of Renameable Horn Backdoors (SK, MK, CS), pp. 154–160.

ICLP-2007-Nguyen #approximate #complexity #knowledge base #logic

Approximating Horn Knowledge Bases in Regular Description Logics to Have PTIME Data Complexity (LAN), pp. 438–439.

SAT-2007-LangloisST #bound

Horn Upper Bounds and Renaming (ML, RHS, GT), pp. 80–93.

SAT-2007-MakinoTY #on the #problem

On the Boolean Connectivity Problem for Horn Relations (KM, ST, MY), pp. 187–200.

PPDP-2006-Miller #analysis #horn clause #source code

Collection analysis for Horn clause programs (DM), pp. 179–188.

SAT-2006-BubeckB #complexity #dependence #modelling #quantifier

Dependency Quantified Horn Formulas: Models and Complexity (UB, HKB), pp. 198–211.

PADL-2005-WangGL #code generation #continuation #logic #semantics #towards

Towards Provably Correct Code Generation via Horn Logical Continuation Semantics (QW, GG, ML), pp. 98–112.

SAT-J-2004-PorschenS05 #bound #problem

Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems (SP, ES), pp. 251–262.

CADE-2005-VermaSS #complexity #equation #horn clause #on the

On the Complexity of Equational Horn Clauses (KNV, HS, TS), pp. 337–352.

ICLP-2005-Ray #horn clause #logic #query

The Need for Ancestor Resolution When Answering Queries in Horn Clause Logic (OR), pp. 410–411.

ICLP-2005-Santos #concurrent #logic #semantics #transaction #using

Denotational Semantics Using Horn Concurrent Transaction Logic (MVS), pp. 431–432.

SAT-2005-BubeckBZ #equivalence #modelling #quantifier

Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas (UB, HKB, XZ), pp. 386–392.

SAT-2005-Coste-MarquisBL #branch #heuristic #quantifier

A Branching Heuristics for Quantified Renamable Horn Formulas (SCM, DLB, FL), pp. 393–399.

SAT-2004-NishimuraRS #detection #set

Detecting Backdoor Sets with Respect to Horn and Binary Clauses (NN, PR, SS), pp. 96–103.

LOPSTR-2003-WangG #continuation #horn clause #semantics

Continuation Semantics as Horn Clauses (QW, GG), pp. 176–177.

CSL-2003-EiterM #abduction #generative #query

Generating All Abductive Explanations for Queries on Propositional Horn Theories (TE, KM), pp. 197–211.

SAT-2003-BuningSZ #modelling #on the #quantifier

On Boolean Models for Quantified Boolean Horn Formulas (HKB, KS, XZ), pp. 93–104.

VMCAI-2003-OgataF #protocol #verification

Formal Verification of the Horn-Preneel Micropayment Protocol (KO, KF), pp. 238–252.

WRLA-2002-ClavelMP #equation #logic #similarity

Reflection in Membership Equational Logic, Many-Sorted Equational Logic, Horn Logic with Equality, and Rewriting Logic (MC, JM, MP), pp. 110–126.

SAS-2002-NielsonNS #horn clause #normalisation

Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi (FN, HRN, HS), pp. 20–35.

ICLP-2002-MaSX #logic programming #source code

The Limits of Horn Logic Programs (SM, YS, KX), p. 467.

SAS-2001-GlynnSS #analysis #constraints #effectiveness #strict

Effective Strictness Analysis with HORN Constraints (KG, PJS, MS), pp. 73–92.

CSL-2001-Kanovich #linear #logic #monad #power of

The Expressive Power of Horn Monadic Linear Logic (MIK), pp. 39–53.

ICML-2000-Khardon #learning

Learning Horn Expressions with LogAn-H (RK), pp. 471–478.

CL-2000-Pliuskevicius #deduction #on the #strict

On an ω-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL (RP), pp. 523–537.

ICML-1998-ReddyT #first-order #learning #source code

Learning First-Order Acyclic Horn Programs from Entailment (CR, PT), pp. 472–480.

CADE-1998-OhtaIH #on the #testing

On the Relationship Between Non-Horn Magic Sets and Relevancy Testing (YO, KI, RH), pp. 333–348.

JICSLP-1998-Gupta #logic

Horn Logic Denotations (GG), pp. 357–358.

LICS-1998-CharatonikMNPW #calculus #μ-calculus

The Horn μ-calculus (WC, DAM, DN, AP, IW), pp. 58–69.

CADE-1997-HasegawaIOK #bottom-up #proving #set #theorem proving #top-down

Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.

ICML-1996-JappyNG #horn clause #learning #robust #source code

Negative Robust Learning Results from Horn Clause Programs (PJ, RN, OG), pp. 258–265.

LOPSTR-1995-Aarts #complexity #source code

Complexity of Horn Programs (EA), pp. 76–90.

LOPSTR-1995-ParkesW #horn clause #induction #logic programming #synthesis

Logic Program Synthesis by Induction over Horn Clauses (AJP, GAW), p. 170.

ICLP-1995-DegtyarevV #horn clause #similarity

A New Procedural Interpretation of Horn Clauses with Equality (AD, AV), pp. 565–579.

SEKE-1994-CookeDGK #concurrent #linear #logic programming #source code

Bag languages, concurrency, Horn logic programs, and linear logic (DEC, RD, AQG, VK), pp. 289–297.

ALP-1994-AlpuenteFV #analysis #composition #equation #source code

Compositional Analysis for Equational Horn Programs (MA, MF, GV), pp. 77–94.

PODS-1993-Schaerf #database

Negation and Minimality in Non-Horn Databases (MS), pp. 147–157.

ICML-1993-FrazierP #learning

Learning From Entailment: An Application to Propositional Horn Sentences (MF, LP), pp. 120–127.

CSL-1993-Marcinkowski #decidability #horn clause #set

A Horn Clause that Implies and Undecidable Set of Horn Clauses (JM), pp. 223–237.

ILPS-1993-DevienneLR #decidability #horn clause #problem #recursion

The Emptiness Problem of One Binary Recursive Horn Clause is Undecidable (PD, PL, JCR), pp. 250–265.

KR-1992-GreinerS #approximate #learning

Learning Useful Horn Approximations (RG, DS), pp. 383–392.

LICS-1992-Kanovich #linear #logic #programming

Horn Programming in Linear Logic Is NP-Complete (MIK), pp. 200–210.

ICALP-1991-Dershowitz #horn clause #set

Cononical Sets of Horn Clauses (ND), pp. 267–278.

ISLP-1991-Wadge #higher-order #logic programming

Higher-Order Horn Logic Programming (WWW), pp. 289–303.

ICSE-1990-GanzingerS #composition #horn clause #order #specification

System Support for Modular Order-Sorted Horn Clause Specifications (HG, RS), pp. 150–159.

CADE-1990-WakayamaP #abstraction #source code

Case-Free Programs: An Abstraction of Definite Horn Programs (TW, THP), pp. 87–101.

CLP-1990-SchreyeVB90 #detection #graph #horn clause #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.

PODS-1989-Grahne #database #performance

Horn Tables — An Efficient Tool for Handling Incomplete Information in Databases (GG), pp. 75–82.

ICALP-1989-TuckerZ #source code

Horn Programs and Semicomputable Relations on Abstract Structures (JVT, JIZ), pp. 745–760.

CSL-1989-Leitsch

Deciding Horn Classes by Hyperresolution (AL), pp. 225–241.

LICS-1989-BoseCLM #horn clause #named #parallel #proving #theorem proving

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.

NACLP-1989-DungK #on the #source code

On the Generalized Predicate Completion of Non-Horn Programs (PMD, KK), pp. 587–603.

VLDB-1988-KrishnamurthyN #horn clause #towards

Towards a Real Horn Clause Language (RK, SAN), pp. 252–263.

VLDB-1988-Lozinskii #deduction

Computing Facts in Non-Horn Deductive Systems (ELL), pp. 273–279.

ALP-1988-LiuL #fuzzy #horn clause #reasoning

Fuzzy Reasoning Based on F-Horn Clause Rules (DL, DL), pp. 214–222.

CADE-1988-AllenBCM #horn clause #named #parallel #proving #theorem proving

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.

CADE-1988-ChiH #horn clause #query #recursion

Recursive Query Answering with Non-Horn Clauses (SC, LJH), pp. 294–312.

CADE-1988-KounalisR #on the #problem #word

On Word Problems in Horn Theories (EK, MR), pp. 527–537.

CADE-1988-MinkerR #logic programming #source code

Procedural Interpretation of Non-Horn Logic Programs (JM, AR), pp. 278–293.

CSL-1988-Schatz

Delete Operations and Horn Formulas (RS), pp. 329–343.

JICSCP-1988-LoboMR88 #source code

Weak Completion Theory for Non-Horn Programs (JL, JM, AR), pp. 828–842.

JICSCP-1988-Nystrom88 #horn clause

Control Structures for Guarded Horn Clauses (SON), pp. 1351–1370.

JICSCP-1988-SmithL88 #interpreter #prolog

A Simple Near-Horn Prolog Interpreter (BTS, DWL), pp. 794–809.

PODS-1987-RamakrishnanBS #horn clause #infinity #recursion #safety

Safety of Recursive Horn Clauses With Infinite Relations (RR, FB, AS), pp. 328–339.

CSL-1987-KarpinskiBS #complexity #horn clause #on the #quantifier

On the Computational Complexity of Quantified Horn Clauses (MK, HKB, PHS), pp. 129–137.

ICLP-1987-Loveland87 #prolog

Near-Horn PROLOG (DWL), pp. 456–469.

ICLP-1987-SaccaZ87 #implementation #logic #query #recursion

Implementation of Recursive Queries for a Data Language Based on Pure Horn Logic (DS, CZ), pp. 104–135.

ICLP-1987-ShmueliN87 #horn clause #set #source code

Set Grouping and Layering in Horn Clause Programs (OS, SAN), pp. 152–177.

CADE-1986-Dietrich #algebra #logic

Relating Resolution and Algebraic Completion for Horn Logic (RD), pp. 62–78.

ICLP-1986-Abdallah86 #programming

Procedures in Horn-Clause Programming (MANA), pp. 433–447.

SLP-1986-GallierR86 #horn clause #similarity

SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification (JHG, SR), pp. 168–179.

PODS-1982-ChandraH #fixpoint #horn clause #query

Horn Clauses and the Fixpoint Query Hierarchy (AKC, DH), pp. 158–163.

CADE-1982-HenschenN #database #first-order #infinity #recursion #representation #sequence

Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases (LJH, SAN), pp. 342–359.

ILPC-1982-Monteiro82 #concurrent #horn clause #logic #specification

A Horn Clause-like Logic for Specifying Concurrency (LM), pp. 1–8.

STOC-1980-Fagin #database #dependence #horn clause

Horn Clauses and Database Dependencies (Extended Abstract) (RF), pp. 123–134.