Littérature scientifique sur le sujet « Craig's interpolation »
Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres
Sommaire
Consultez les listes thématiques d’articles de revues, de livres, de thèses, de rapports de conférences et d’autres sources académiques sur le sujet « Craig's interpolation ».
À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.
Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.
Articles de revues sur le sujet "Craig's interpolation"
Beklemishev, L. D. « Provability logic without Craig's interpolation property ». Mathematical Notes of the Academy of Sciences of the USSR 45, no 6 (juin 1989) : 437–45. http://dx.doi.org/10.1007/bf01158230.
Texte intégralMaffezioli, Paolo, et Eugenio Orlandelli. « Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate ». Bulletin of the Section of Logic 48, no 2 (30 juin 2019) : 137–58. http://dx.doi.org/10.18778/0138-0680.48.2.04.
Texte intégralSági, Gábor, et Saharon Shelah. « On weak and strong interpolation in algebraic logics ». Journal of Symbolic Logic 71, no 1 (mars 2006) : 104–18. http://dx.doi.org/10.2178/jsl/1140641164.
Texte intégralMason, Ian. « The metatheory of the classical propositional calculus is not axiomatizable ». Journal of Symbolic Logic 50, no 2 (juin 1985) : 451–57. http://dx.doi.org/10.2307/2274233.
Texte intégralOno, Hiroakira. « Craig's interpolation theorem for the intuitionistic logic and its extensions—A semantical approach ». Studia Logica 45, no 1 (mars 1986) : 19–33. http://dx.doi.org/10.1007/bf01881546.
Texte intégralALIZADEH, MAJID, FARZANEH DERAKHSHAN et HIROAKIRA ONO. « UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS ». Review of Symbolic Logic 7, no 3 (27 mai 2014) : 455–83. http://dx.doi.org/10.1017/s175502031400015x.
Texte intégralRodenburg, P. H. « Interpolation in Conditional Equational Logic1 ». Fundamenta Informaticae 15, no 1 (1 juin 1991) : 80–85. http://dx.doi.org/10.3233/fi-1991-15106.
Texte intégralMolnár, Zalán, et Öztürk Övge. « Notes on localizing Craig’s interpolation theorem ». Elpis. Filozófiatudományi Folyóirat 15, no 1-2 (2022) : 103–16. http://dx.doi.org/10.54310/elpis.2022.1.8.
Texte intégralKowalski, Tomasz. « PDL has interpolation ». Journal of Symbolic Logic 67, no 3 (septembre 2002) : 933–46. http://dx.doi.org/10.2178/jsl/1190150141.
Texte intégralFeferman, Solomon. « Harmonious logic : Craig’s interpolation theorem and its descendants ». Synthese 164, no 3 (1 juillet 2008) : 341–57. http://dx.doi.org/10.1007/s11229-008-9354-2.
Texte intégralThèses sur le sujet "Craig's interpolation"
Weissenbacher, Georg. « Program analysis with interpolants ». Thesis, University of Oxford, 2010. http://ora.ox.ac.uk/objects/uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6.
Texte intégralBarbier, Fabrice. « Résultats de théorie abstraite des modèles dans le cadre des institutions : vers la combinaison de logiques ». Phd thesis, Université d'Evry-Val d'Essonne, 2005. http://tel.archives-ouvertes.fr/tel-00087587.
Texte intégralXiong, Li-Yu, et 熊立宇. « Craig Interpolation Theorem ». Thesis, 2009. http://ndltd.ncl.edu.tw/handle/87462903790124238437.
Texte intégral國立中正大學
哲學所
97
In this paper we will survey two different proofs of the Craig interpolation theorem. In the first order logic, the Craig interpolation theorem is a useful result about the connection between two theories. Roughly speaking, for any two sentences φ and ψ with φ│=ψ, there exists a sentence θ, called an interpolant, such that φ│=θ and θ│=ψ, where φ and ψ can belong to two different languages, and the interpolant θ only uses the common part of two languages of φ and ψ. That is, the logical entailment φ│=ψ can be achieved through some interpolant θ (from their common part) by φ│=θ and θ│=ψ. The Craig interpolation theorem was first proved by William Craig in 1957. In chapter I, we introduce basic knowledge of model theory. In chapter II, we follow the approach of Chang-Keisler, which resembles the proof of the completeness theorem to prove the Craig interpolation theorem by the inseparable method. In chapter III, we take a game-theoretic approach to prove the Craig interpolation theorem by the back-and-forth argument (see Doets).
Lin, Hsuan-Po, et 林炫伯. « Large Scale Ashenhurst Decomposition via SAT Solving and Craig Interpolation ». Thesis, 2009. http://ndltd.ncl.edu.tw/handle/91435812875963719114.
Texte intégral國立臺灣大學
電子工程學研究所
97
Functional decomposition aims at decomposing a Boolean function into a set of smaller sub-functions. In this thesis, we focus on Ashenhurst decomposition, which has practical applications due to its simplicity. We formulate the decomposition problem as SAT solving, and further apply Craig interpolation and functional dependency computation to derive composite functions. In our pure SAT-based solution, variable partitioning can be automated and integrated into the decomposition procedure. Also we can easily extend our method to non-disjoint and multiple-output decompositions which are hard to handle using BDD-based algorithms. Experimental results show the scalability of our proposed method, which can effectively decompose functions with up to 300 input variables.
Lin, Ting-Hao, et 林庭豪. « Using SAT-based Craig Interpolation to Enlarge Clock Gating Functions ». Thesis, 2011. http://ndltd.ncl.edu.tw/handle/29140781507819471872.
Texte intégral國立臺灣大學
電機工程學研究所
99
Dynamic power saving is gaining its dominance in modern low power designs, while clock gating, which blocks unnecessary clock switching activities, is one of the most efficient approaches to reduce the dynamic power. In this thesis, we exploit the interpolation technique in a SAT-based clock gating algorithm in order to grant a greater flexibility in enlarging the gating capabilities over the original gating candidates. We also developed several techniques to improve the runtime and memory usage of the clock gating algorithm, including a gating capability filter to reduce the number of formal SAT proofs, a dynamic backtracking limit controller to shorten the SAT runs, and a shrinking method to ease the final gate count overhead. The experimental results show that our proposed algorithm can gate up to 2X clock switches with less than 5% area overhead when compared to the state-of-the-art SAT-based clock gating methodology.
Han, Cheng-Shen, et 韓承駪. « A Study of Gaussian Elimination on Boolean Satisfiability and Craig Interpolation ». Thesis, 2012. http://ndltd.ncl.edu.tw/handle/86700561504561244362.
Texte intégral國立臺灣大學
電子工程學研究所
100
The Boolean satisfiability problem (SAT) is one of the central problems in computer science of both theoretical and practical interests. SAT is the first discovered NP-complete problem, and many real-world computation problems, such as hardware and software verification, electronic design automation (EDA), artificial intelligence (AI), circuit design, automatic theorem proving, etc., can be naturally encoded as SAT instances and solved efficiently. Although impressive advancements of SAT solving have been achieved, recent research reveals modern solvers'' inability to handle formulae in the abundance of parity xor constraints. Although xor-handling in SAT solving has attracted much attention, challenges remain to completely deduce xor-inferred implications and conflicts, to effectively reduce expensive overhead, and to directly generate compact interpolants. This thesis presents a new SAT solver, SimpSat, which integrates SAT solving tightly with Gaussian elimination in the style of Dantzig''s simplex method. It yields a powerful tool overcoming these challenges. Experiments show promising performance improvements and efficient derivation of compact interpolants, which are otherwise unobtainable.
Rocchetto, Marco. « Methods and tools for design time and runtime formal analysis of security protocols and web applications ». Doctoral thesis, 2015. http://hdl.handle.net/11562/913185.
Texte intégralThe increasing complexity of web applications together with their underling security protocols has rapidly increased the need of automatic security analysis methods and tools. In this thesis, I address this problem by proposing two new formal approaches for the security verification of security protocols and web applications. The first is a design time interpolation-based method for security protocol verification. This method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev-Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. The second is a runtime (model-based) security analysis technique that searches for logic and implementation flaws on concrete (web-based) systems. In particular, I focused on how to use the Dolev-Yao intruder model to search for Cross-Site Request Forgery (CSRF) attacks. CSRF is listed in the top ten list of the Open Web Application Security Project (OWASP) as one of the most critical threats to web security.
Jančík, Pavel. « Reprezentace stavů programu ». Doctoral thesis, 2017. http://www.nusl.cz/ntk/nusl-369534.
Texte intégralBlicha, Martin. « Metody pro redukci velikosti interpolantů při použití částečného přiřazení ». Master's thesis, 2016. http://www.nusl.cz/ntk/nusl-352598.
Texte intégralChapitres de livres sur le sujet "Craig's interpolation"
Huang, Guoxiang. « Constructing Craig interpolation formulas ». Dans Lecture Notes in Computer Science, 181–90. Berlin, Heidelberg : Springer Berlin Heidelberg, 1995. http://dx.doi.org/10.1007/bfb0030832.
Texte intégralMcMillan, Ken L. « Craig Interpolation and Reachability Analysis ». Dans Static Analysis, 336. Berlin, Heidelberg : Springer Berlin Heidelberg, 2003. http://dx.doi.org/10.1007/3-540-44898-5_18.
Texte intégralBrotherston, James, et Rajeev Goré. « Craig Interpolation in Displayable Logics ». Dans Lecture Notes in Computer Science, 88–103. Berlin, Heidelberg : Springer Berlin Heidelberg, 2011. http://dx.doi.org/10.1007/978-3-642-22119-4_9.
Texte intégralGheerbrant, Amélie, et Balder ten Cate. « Craig Interpolation for Linear Temporal Languages ». Dans Computer Science Logic, 287–301. Berlin, Heidelberg : Springer Berlin Heidelberg, 2009. http://dx.doi.org/10.1007/978-3-642-04027-6_22.
Texte intégralJaakkola, Reijo. « Uniform Guarded Fragments ». Dans Lecture Notes in Computer Science, 409–27. Cham : Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-030-99253-8_21.
Texte intégralGhilardi, Silvio, Alessandro Gianola et Deepak Kapur. « Interpolation and Amalgamation for Arrays with MaxDiff ». Dans Lecture Notes in Computer Science, 268–88. Cham : Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-71995-1_14.
Texte intégralCarbone, A. « The Craig Interpolation Theorem for Schematic Systems ». Dans Collegium Logicum, 87–100. Vienna : Springer Vienna, 1996. http://dx.doi.org/10.1007/978-3-7091-9461-4_6.
Texte intégralMcMillan, Kenneth. « Applications of Craig Interpolation to Model Checking ». Dans Computer Science Logic, 22–23. Berlin, Heidelberg : Springer Berlin Heidelberg, 2004. http://dx.doi.org/10.1007/978-3-540-30124-0_3.
Texte intégralMcMillan, Kenneth. « Applications of Craig Interpolation to Model Checking ». Dans Applications and Theory of Petri Nets 2005, 15–16. Berlin, Heidelberg : Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/11494744_2.
Texte intégralTeige, Tino, et Martin Fränzle. « Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems ». Dans Tools and Algorithms for the Construction and Analysis of Systems, 158–72. Berlin, Heidelberg : Springer Berlin Heidelberg, 2011. http://dx.doi.org/10.1007/978-3-642-19835-9_14.
Texte intégralActes de conférences sur le sujet "Craig's interpolation"
Lin, Ting-Hao, et Chung-Yang (Ric) Huang. « Using SAT-based Craig interpolation to enlarge clock gating functions ». Dans the 48th Design Automation Conference. New York, New York, USA : ACM Press, 2011. http://dx.doi.org/10.1145/2024724.2024867.
Texte intégralSauer, Matthias, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar Reddy et Bernd Becker. « Functional test of small-delay faults using SAT and Craig interpolation ». Dans 2012 IEEE International Test Conference (ITC). IEEE, 2012. http://dx.doi.org/10.1109/test.2012.6401550.
Texte intégralSauer, Matthias, Stefan Kupferschmid, Alexander Czutro, Sudhakar Reddy et Bernd Becker. « Analysis of Reachable Sensitisable Paths in Sequential Circuits with SAT and Craig Interpolation ». Dans 2012 25th International Conference on VLSI Design. IEEE, 2012. http://dx.doi.org/10.1109/vlsid.2012.101.
Texte intégralScholl, Christoph, Stefan Disch, Florian Pigorsch et Stefan Kupferschmid. « Using an SMT solver and Craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra ». Dans the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop. New York, New York, USA : ACM Press, 2008. http://dx.doi.org/10.1145/1512464.1512469.
Texte intégralFortin, Marie, Boris Konev et Frank Wolter. « Interpolants and Explicit Definitions in Extensions of the Description Logic EL ». Dans 19th International Conference on Principles of Knowledge Representation and Reasoning {KR-2022}. California : International Joint Conferences on Artificial Intelligence Organization, 2022. http://dx.doi.org/10.24963/kr.2022/16.
Texte intégralRapports d'organisations sur le sujet "Craig's interpolation"
Jain, Himanshu, Edmund M. Clarke et Orna Grumberg. Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. Fort Belvoir, VA : Defense Technical Information Center, février 2008. http://dx.doi.org/10.21236/ada476801.
Texte intégral