Stem claus$ (all stems)

160 papers:

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.

CADE-2015-GorznyP #first-order #proving #towards

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (JG, BWP), pp. 356–366.

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-AnsoteguiGLS #community #detection #using

Using Community Structure to Detect Relevant Learnt Clauses (CA, JGC, JL, LS), pp. 238–254.

SAT-2015-LonsingE #api #incremental #satisfiability

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API (FL, UE), pp. 191–198.

SAT-2015-TuHJ #learning #named #reasoning #satisfiability

QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (KHT, TCH, JHRJ), pp. 343–359.

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

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

DATE-2014-CabodiPQV #approximate #reachability #satisfiability

Tightening BDD-based approximate reachability with SAT-based clause generalization∗ (GC, PP, SQ, DV), pp. 1–6.

SAT-2014-AudemardS #lazy evaluation #parallel #policy #satisfiability

Lazy Clause Exchange Policy for Parallel SAT Solvers (GA, LS), pp. 197–205.

SAT-2014-BalintBFS #heuristic #implementation #satisfiability

Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses (AB, AB, AF, US), pp. 302–316.

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

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

CADE-2013-AzmyW #normalisation

Computing Tiny Clause Normal Forms (NA, CW), pp. 109–125.

CADE-2013-HoderV

The 481 Ways to Split a Clause and Deal with Propositional Variables (KH, AV), pp. 450–464.

CADE-2013-KersaniP #decidability #first-order

Completeness and Decidability Results for First-Order Clauses with Indices (AK, NP), pp. 58–75.

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.

SAT-2013-Johannsen #exponential #learning #proving

Exponential Separations in a Hierarchy of Clause Learning Proof Systems (JJ), pp. 40–51.

SAT-2013-LonsingEG #learning #performance #pseudo #quantifier

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation (FL, UE, AVG), pp. 100–115.

SAT-2013-MantheyPW #satisfiability

Soundness of Inprocessing in Clause Sharing SAT Solvers (NM, TP, CW), pp. 22–39.

SAT-2013-WieringaH #concurrent

Concurrent Clause Strengthening (SW, KH), pp. 116–132.

FASE-2012-BradfieldS #calculus #qvt #recursion #μ-calculus

Recursive Checkonly QVT-R Transformations with General when and where Clauses via the Modal μ Calculus (JCB, PS), pp. 194–208.

FoSSaCS-2012-SeidlR

Extending H₁-Clauses with Path Disequalities (HS, AR), pp. 165–179.

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.

CIAA-2012-ReussS

Crossing the Syntactic Barrier: Hom-Disequalities for H1-Clauses (AR, HS), pp. 301–312.

SAT-2012-AudemardHJLP #parallel #satisfiability

Revisiting Clause Exchange in Parallel SAT Solving (GA, BH, SJ, JML, CP), pp. 200–213.

SAT-2012-BonetB #learning

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (MLB, SRB), pp. 44–57.

SAT-2012-KullmannZ #on the #reduction #satisfiability

On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets (OK, XZ), pp. 270–283.

SAT-2012-LaitinenJN #learning

Conflict-Driven XOR-Clause Learning (TL, TAJ, IN), pp. 383–396.

SAT-2012-LiWL #satisfiability

Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability — (Poster Presentation) (CML, WW, YL), pp. 479–480.

SAT-2012-MatsliahSS #learning

Augmenting Clause Learning with Implied Literals — (Poster Presentation) (AM, AS, HS), pp. 500–501.

SAT-2012-SabharwalSS #learning #satisfiability

Learning Back-Clauses in SAT — (Poster Presentation) (AS, HS, MS), pp. 498–499.

DATE-2011-HanJS #analysis

Clause simplification through dominator analysis (HH, HJ, FS), pp. 143–148.

PLDI-2011-JoseM #fault #locality #satisfiability #using

Cause clue clauses: error localization using maximum satisfiability (MJ, RM), pp. 437–446.

STOC-2011-Svensson

Santa Claus schedules jobs on unrelated machines (OS), pp. 617–626.

CIAA-2011-CastanoC #approach #satisfiability

Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability (JMC, RC), pp. 76–87.

CADE-2011-BiereLS

Blocked Clause Elimination for QBF (AB, FL, MS), pp. 101–115.

CADE-2011-Horbach #horn clause #set

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

SAT-2011-AudemardLMS #on the

On Freezing and Reactivating Learnt Clauses (GA, JML, BM, LS), pp. 188–200.

SAT-2011-Gelder11a #satisfiability

Generalized Conflict-Clause Strengthening for Satisfiability Solvers (AVG), pp. 329–342.

DRR-2010-ChazalonC #definite clause grammar #documentation #using

Using definite clause grammars to build a global system for analyzing collections of documents (JC, BC), pp. 1–10.

FASE-2010-LehnerM #performance #runtime

Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups (HL, PM), pp. 338–352.

TACAS-2010-JarvisaloBH

Blocked Clause Elimination (MJ, AB, MH), pp. 129–144.

KR-2010-DelgrandeW #horn clause #set

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

ICLP-2010-SaeedloeiG10 #definite clause grammar

Timed Definite Clause Ω-Grammars (NS, GG), pp. 212–221.

SAT-2010-Ben-SassonJ #bound #learning #strict

Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas (EBS, JJ), pp. 16–29.

SAT-2010-JarvisaloB

Reconstructing Solutions after Blocked Clause Elimination (MJ, AB), pp. 340–345.

CADE-2009-GregoireMP #question #set

Does This Set of Clauses Overlap with at Least One MUS? (ÉG, BM, CP), pp. 100–115.

RTA-2009-SeidlV #protocol

Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case (HS, KNV), pp. 118–132.

SAT-2009-AtseriasFT #algorithm #bound

Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution (AA, JKF, MT), pp. 114–127.

SAT-2009-Gelder #proving

Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces (AVG), pp. 141–146.

SAT-2009-HanS #on the fly

On-the-Fly Clause Improvement (HH, FS), pp. 209–222.

SAT-2009-Johannsen #bound #exponential #learning #strict

An Exponential Lower Bound for Width-Restricted Clause Learning (JJ), pp. 128–140.

SAT-2009-PipatsrisawatD #policy #satisfiability

Width-Based Restart Policies for Clause-Learning Satisfiability Solvers (KP, AD), pp. 341–355.

SAT-2009-SorenssonB

Minimizing Learned Clauses (NS, AB), pp. 237–243.

ESOP-2008-NielsenNN #horn clause

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

ICML-2008-KuzelkaZ #estimation #first-order #performance

Fast estimation of first-order clause coverage through randomization and maximum likelihood (OK, FZ), pp. 504–511.

KR-2008-Delgrande #horn clause

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

KR-2008-Rintanen #graph

Planning Graphs and Propositional Clause-Learning (JR), pp. 535–543.

SAT-2008-LiffitonS #satisfiability #set

Searching for Autarkies to Trim Unsatisfiable Clause Sets (MHL, KAS), pp. 182–195.

SAT-2008-StachniakB #learning #satisfiability

Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning (ZS, AB), pp. 257–270.

DATE-2007-SafarSES #configuration management #interactive #satisfiability

Interactive presentation: A shift register based clause evaluator for reconfigurable SAT solver (MS, MS, MWEK, AS), pp. 153–158.

CADE-2007-Lev-AmiWRS

Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.

ICLP-2007-CostaSL #prolog

Demand-Driven Indexing of Prolog Clauses (VSC, KFS, RL), pp. 395–409.

SAT-2007-ArgelichM #learning #satisfiability

Partial Max-SAT Solvers with Clause Learning (JA, FM), pp. 28–40.

SAT-2007-Kullmann #invariant #matrix #polynomial #satisfiability

Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices (OK), pp. 314–327.

STOC-2006-BansalS #problem

The Santa Claus problem (NB, MS), pp. 31–40.

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

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

SAT-2006-DantsinW #constant #performance #satisfiability

MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(s2) Time (ED, AW), pp. 266–276.

SAT-2006-KullmannLM #agile #categorisation #kernel #normalisation #satisfiability

Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel (OK, IL, JMS), pp. 22–35.

SAT-2006-SamulowitzB #reasoning

Binary Clause Reasoning in QBF (HS, FB), pp. 353–367.

DAC-2005-JinS #performance

Prime clauses for fast enumeration of satisfying assignments to boolean circuits (HJ, FS), pp. 750–753.

SAT-J-2004-JacksonS05

Clause Form Conversions for Boolean Circuits (PJ, DS), pp. 183–198.

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.

SAT-2005-DershowitzHN #heuristic #satisfiability

A Clause-Based Heuristic for SAT Solvers (ND, ZH, AN), pp. 46–60.

SAT-2005-EenB #effectiveness #preprocessor #satisfiability

Effective Preprocessing in SAT Through Variable and Clause Elimination (NE, AB), pp. 61–75.

SAT-2004-NishimuraRS #detection #set

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

SAT-2004-SangBBKP #component #effectiveness #learning

Combining Component Caching and Clause Learning for Effective Model Counting (TS, FB, PB, HAK, TP), pp. 20–28.

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

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

CADE-2003-GanzingerS #equivalence #normalisation #reasoning

Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation (HG, JS), pp. 335–349.

SAT-2003-BaumerS #algorithm #independence #probability #satisfiability

Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs (SB, RS), pp. 150–161.

SAT-2003-Kullmann #combinator

The Combinatorics of Conflicts between Clauses (OK), pp. 426–440.

SAT-2003-SabharwalBK #learning #performance #problem #using

Using Problem Structure for Efficient Clause Learning (AS, PB, HAK), pp. 242–256.

VMCAI-2003-CatanoH #ml #named #static analysis

CHASE: A Static Checker for JML’s Assignable Clause (NC, MH), pp. 26–40.

DAC-2002-PilarskiH #satisfiability

SAT with partial clauses and back-leaps (SP, GH), pp. 743–746.

SAS-2002-NielsonNS #horn clause #normalisation

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

SAT-2002-DuboisD #random #satisfiability

Renormalization as a function of clause lengths for solving random k-SAT formulae (OD, GD), p. 15.

SAT-2002-Gelder #reasoning #satisfiability #towards

Toward leaner binary-clause reasoning in a satisfiability solver (AVG), p. 16.

SAT-2002-HirschK #named #satisfiability

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination (EH, AK), p. 38.

SAT-2002-ZhaoB #equivalence #problem

Extension and equivalence problems for clause minimal formulas (XZ, HKB), p. 43.

DAC-2001-GuptaGYA #detection #image #satisfiability

Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation (AG, AG, ZY, PA), pp. 536–541.

ICLP-2001-HoweK #multi

Positive Boolean Functions as Multiheaded Clauses (JMH, AK), pp. 120–134.

CADE-1998-NonnengartRW #generative #normalisation #on the

On Generating Small Clause Normal Forms (AN, GR, CW), pp. 397–411.

CADE-1997-Bonacina #proving #theorem proving

The Clause-Diffusion Theorem Prover Peers-mcd (System Description) (MPB), pp. 53–56.

CADE-1997-NieuwenhuisRV #algorithm #automation #data type #deduction #kernel #named #similarity

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses (RN, JMR, MÁV), pp. 49–52.

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

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

JICSLP-1996-Chau #definite clause grammar #specification

Specification of Complex Systems with Definite Clause Grammar (Poster Abstract) (HLC), p. 544.

DAC-1995-RohfleischWA #analysis #logic #optimisation

Logic Clause Analysis for Delay Optimization (BR, BW, KA), pp. 668–672.

OOPSLA-1995-DayGLM #morphism #parametricity #polymorphism #type system

Subtypes vs. Where Clauses: Constraining Parametric Polymorphism (MD, RG, BL, ACM), pp. 156–168.

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.

ILPS-1995-DawsonRRS #optimisation #unification

Optimizing Clause Resolution: Beyond Unification Factoring (SD, CRR, IVR, TS), pp. 194–208.

ILPS-1995-Hui-Bon-Hoa #proving

Clause-based proofs for hereditary Harrop formulas (AHBH), pp. 179–193.

KR-1994-Eugenio #natural language #representation

Action Representation for Interpreting Purpose Clauses in Natural Language Instructions (BDE), pp. 158–169.

PLILP-1994-Barklund #source code

Tabulation of Functions in Definite Clause Programs (JB), pp. 465–466.

PLILP-1994-GergatsoulisK #source code

Unfold/Fold Transformations For Definite Clause Programs (MG, MK), pp. 340–354.

CADE-1994-Salzer #unification

Primal Grammars and Unification Modulo a Binary Clause (GS), pp. 282–295.

CADE-1994-WirthG #equation #induction #on the

On Notions of Inductive Validity for First-Oder Equational Clauses (CPW, BG), pp. 162–176.

ICLP-1994-Christiansen #performance

Efficient and Complete Demo Predicates for Definite Clause Languages (HC), pp. 735–736.

ICLP-1994-JacquetM #named

PP-clauses: A Means for Handling Resources (JMJ, LM), p. 743.

LICS-1994-BaazFL #proving

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation (MB, CGF, AL), pp. 213–219.

FME-1993-ParkinW

Conformity Clause for VDM-SL (GIP, BAW), pp. 501–520.

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.

ILPS-1993-Felty #definite clause grammar #higher-order #parsing #syntax

Definite Clause Grammars for Parsing Higher-Order Syntax (APF), p. 668.

ILPS-1993-Spencer #order #strict

The Ordered Clause Restriction of Model Elimination and SLI Resolution (BS), p. 678.

ILPS-1993-WaalG #logic programming

Logic Program Specialisation With Deletion of Useless Clauses (DAdW, JPG), p. 632.

RTA-1993-NivelaN #first-order

Saturation of First-Order (Constrained) Clauses with the Saturate System (PN, RN), pp. 436–440.

CADE-1992-NieuwenhuisR #proving #theorem proving

Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.

JICSLP-1992-HaasJ #definite clause grammar #interactive #synthesis

Interactive Synthesis of Definite-Clause Grammars (JH, BJ), pp. 541–555.

JICSLP-1992-JacquetM #communication #logic programming #towards

Communicating Clauses: Towards Synchronous Communication in Contextual Logic Programming (JMJ, LM), pp. 98–112.

ICALP-1991-Dershowitz #horn clause #set

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

POPL-1990-RameshRW #prolog

Automata-Driven Indexing of Prolog Clauses (RR, IVR, DSW), pp. 281–291.

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

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

CADE-1990-Burckert #constraints

A Resolution Principle for Clauses with Constraints (HJB), pp. 178–192.

CADE-1990-Sutcliffe #proving #theorem proving

A General Clause Theorem Prover (GS), pp. 675–676.

CADE-1990-Tour

Minimizing the Number of Clauses by Renaming (TBdlT), pp. 558–572.

CADE-1990-Wolfram #named

ACE: The Abstract Clause Engine (DAW), pp. 679–680.

CLP-1990-PareschiM90 #definite clause grammar

Extending Definite Clause Grammars with Scoping Constructs (RP, DM), pp. 373–389.

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.

CSL-1990-Fermuller #set

A Resolution Variant Deciding some Classes of Clause Sets (CGF), pp. 128–144.

CSL-1989-StepankovaS #logic programming #source code

Stratification of Definite Clause Programs and of General Logic Programs (OS, PS), pp. 396–408.

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-DemoenMC #prolog

Indexing Prolog Clauses (BD, AM, AC), pp. 1001–1012.

NACLP-1989-Searls #definite clause grammar

Investigating the Linguistics of DNA with Definite Clause Grammars (DBS), pp. 189–208.

VLDB-1988-KrishnamurthyN #horn clause #towards

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

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

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

PLILP-1988-Dang #definite clause grammar #interactive #specification #using

Formal Specification of Interactive Languages Using Definite Clause Grammars (WD), pp. 283–291.

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.

JICSCP-1988-Abramson88 #approach #aspect-oriented #definite clause grammar #metaprogramming

Metarules and an Approach to Conjunction in Definite Clause Translation Grammars: Some Aspects of Grammatical Metaprogramming (HA), pp. 233–248.

JICSCP-1988-Nystrom88 #horn clause

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

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-ShmueliN87 #horn clause #set #source code

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

CADE-1986-Eisinger #graph #what

What You Always Wanted to Know About Clause Graph Resolution (NE), pp. 316–336.

ICLP-1986-Abdallah86 #programming

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

ICLP-1986-Buettner86 #decompiler #performance #prolog

Fast Decompilation of Compiled Prolog Clauses (KAB), pp. 663–670.

ICLP-1986-GoebelFP86 #approach #constraints #reasoning #using

Using Definite Clauses and Integrity Constraints as the Basis for a Theory Formation Approach to Diagnostic Reasoning (RG, KF, DP), pp. 211–222.

SLP-1986-GallierR86 #horn clause #similarity

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

ICALP-1984-Fribourg #equation #programming language

Oriented Equational Clauses as a Programming Language (LF), pp. 162–173.

SLP-1984-Abramson84 #definite clause grammar

Definite Clause Translation Grammars (HA), pp. 233–240.

SLP-1984-WiseP84 #prolog #word

Indexing Prolog Clauses via Superimposed Code Words and Filed Encoded Words (MJW, DMWP), pp. 203–210.

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

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

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.

POPL-1978-AshcroftW #named

Clauses: Scope Structures and Defined Functions in Lucid (EAA, WWW), pp. 17–22.