Thesis (Ph. D.)--Oregon State University, 1972. / Typescript (photocopy). Includes bibliographical references. Also available on the World Wide Web.

There exist well-known varieties of implication, such as strict, intuitionist, three-valued and rigorous, which are non-classical in the sense of being more restrictive than material implication. But there exists also a type of implication, intuitively plausible, which is nonclassical not only in being more restrictive, but in satisfying certain theses which are classically false. These theses are exceedingly venerable, dating back to Aristotle and Boethius, but, despite their plausibility, have been generally rejected by logicians since. It has not been noticed, however, that in Sextus Empiricus reference is made to a species of Stoic implication which fits them perfectly. In this work formal recognition is given to this species of implication, known as connexive implication. It is shown that none of the well-known systems of prepositional logic is connexive, and a new system is accordingly constructed. A proof of consistency is given, and a number of problems posed for further investigation.

by Mei Long. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2003. / Includes bibliographical references (leaves 93-98). / Abstracts in English and Chinese. / Table of Contents --- p.v / Abstract --- p.viii / Acknowledgements --- p.x / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- Satisfiability Problem --- p.1 / Chapter 1.2 --- Motivation of the Research --- p.1 / Chapter 1.3 --- Overview of the Thesis --- p.2 / Chapter 2 --- Satisfiability Problem --- p.4 / Chapter 2.1 --- Satisfiability Problem --- p.5 / Chapter 2.1.1 --- Basic Definition --- p.5 / Chapter 2.1.2 --- Phase Transitions --- p.5 / Chapter 2.2 --- History --- p.6 / Chapter 2.3 --- The Basic Search Algorithm --- p.8 / Chapter 2.4 --- Some Improvements to the Basic Algorithm --- p.9 / Chapter 2.4.1 --- Satz by Chu-Min Li --- p.9 / Chapter 2.4.2 --- Heuristics and Local Search --- p.12 / Chapter 2.4.3 --- Relaxation --- p.13 / Chapter 2.5 --- Benchmarks --- p.14 / Chapter 2.5.1 --- Specific Problems --- p.14 / Chapter 2.5.2 --- Randomly Generated Problems --- p.14 / Chapter 2.6 --- Software and Internet Information for SAT solving --- p.16 / Chapter 2.6.1 --- Stochastic Local Search Algorithms (incomplete) --- p.16 / Chapter 2.6.2 --- Systematic Search Algorithms (complete) --- p.16 / Chapter 2.6.3 --- Some useful Links to SAT Related Sites --- p.17 / Chapter 3 --- Integer Programming Formulation for Logic Problem --- p.18 / Chapter 3.1 --- SAT Problem --- p.19 / Chapter 3.2 --- MAXSAT Problem --- p.19 / Chapter 3.3 --- Logical Inference Problem --- p.19 / Chapter 3.4 --- Weighted Exact Satisfiability Problem --- p.20 / Chapter 4 --- Integer Programming Formulation for SAT Problem --- p.22 / Chapter 4.1 --- From 3-CNF SAT Clauses to Zero-One IP Constraints --- p.22 / Chapter 4.2 --- Integer Programming Model for 3-SAT --- p.23 / Chapter 4.3 --- The Equivalence of the SAT and the IP --- p.23 / Chapter 4.4 --- Example --- p.24 / Chapter 5 --- Integer Solvability of Linear Programs --- p.27 / Chapter 5.1 --- Unimodularity --- p.27 / Chapter 5.2 --- Totally Unimodularity --- p.28 / Chapter 5.3 --- Some Results on Recognition of Linear Solvability of IP --- p.32 / Chapter 6 --- TU Based Matrix Research Results --- p.33 / Chapter 6.1 --- 2x2 Matrix's TU Property --- p.33 / Chapter 6.2 --- Extended Integer Programming Model for SAT --- p.34 / Chapter 6.3 --- 3x3 Matrix's TU Property --- p.35 / Chapter 7 --- Totally Unimodularity Based Branching-and-Bound Algorithm --- p.38 / Chapter 7.1 --- Introduction --- p.38 / Chapter 7.1.1 --- Enumeration Trees --- p.39 / Chapter 7.1.2 --- The Concept of Branch and Bound --- p.42 / Chapter 7.2 --- TU Based Branching Rule --- p.43 / Chapter 7.2.1 --- How to sort variables based on 2x2 submatrices --- p.43 / Chapter 7.2.2 --- How to sort the rest variables --- p.45 / Chapter 7.3 --- TU Based Bounding Rule --- p.46 / Chapter 7.4 --- TU Based Branch-and-Bound Algorithm --- p.47 / Chapter 7.5 --- Example --- p.49 / Chapter 8 --- Numerical Result --- p.57 / Chapter 8.1 --- Experimental Result --- p.57 / Chapter 8.2 --- Statistical Results of ILOG CPLEX --- p.59 / Chapter 9 --- Conclusions --- p.61 / Chapter 9.1 --- Contributions --- p.61 / Chapter 9.2 --- Future Work --- p.62 / Chapter A --- The Coefficient Matrix A for Example in Chapter 7 --- p.64 / Chapter B --- The Detailed Numerical Information of Solution Process for Exam- ple in Chapter 7 --- p.66 / Chapter C --- Experimental Result --- p.67 / Chapter C.1 --- "# of variables: 20, # of clauses: 91" --- p.67 / Chapter C.2 --- "# of variables: 50, # of clauses: 218" --- p.70 / Chapter C.3 --- # of variables: 75，# of clauses: 325 --- p.73 / Chapter C.4 --- "# of variables: 100, # of clauses: 430" --- p.76 / Chapter D --- Experimental Result of ILOG CPLEX --- p.80 / Chapter D.1 --- # of variables: 20´ة # of clauses: 91 --- p.80 / Chapter D.2 --- # of variables: 50，#of clauses: 218 --- p.83 / Chapter D.3 --- # of variables: 75，# of clauses: 325 --- p.86 / Chapter D.4 --- "# of variables: 100, # of clauses: 430" --- p.89 / Bibliography --- p.93

O uso adequado de ambientes computacionais pode representar um aumento de qualidade e conforto no processo de ensino-aprendizagem de algumas disciplinas. Percebeu-se, através de pesquisa, a inexistência de ferramentas voltadas para o ensino-aprendizagem de cálculo proposicional que atendessem aos critérios estabelecidos para um ambiente de suporte ao aluno (ASA). Como consequência do resultado da pesquisa, este trabalho introduz o conceito e os requisitos básicos de um ASA, concebe e implementa uma ferramenta ASA voltada para o ensino-aprendizagem de cálculo proposicional, acompanhada de um plano de ensino opcional, e os coloca à disposição da comunidade acadêmica. Apresenta também estudos de casos sobre apresentações e usos da ferramenta em vários estágios de desenvolvimento, além da descrição de cada módulo e dos métodos e regras disponibilizados pela ferramenta. Pretende-se que a ferramenta ASA-CalcPro e o plano de ensino sugerido, sejam uma contribuição social positiva e um estímulo ao ensino-aprendizagem de cálculo proposicional. / The adequate use of computational environments can increase the quality and comfort of the teaching-learning process for some of the academic disciplines. A review of the literature reveals the lack of existing tools for the teaching-learning of the propositional calculus that conform to the criteria established for the student support environment (ambiente de suporte ao aluno (ASA)). As a consequence of this conclusion, the current thesis introduces the concept of, and the basic requirements for, an ASA, conceives and implements an ASA tool for the teaching-learning of the propositional calculus, together with an optional teaching plan, and puts both at the disposition of the academic community. The thesis also presents case studies of presentations and uses of the tool at various stages of its development, as well as a description of each module and of the methods and rules made available for use by the tool. It is hoped that the ASA-CalcPro tool and the suggested plan of study will make a positive social contribution and will be a stimulant for the teaching-learning of the propositional calculus.

O uso adequado de ambientes computacionais pode representar um aumento de qualidade e conforto no processo de ensino-aprendizagem de algumas disciplinas. Percebeu-se, através de pesquisa, a inexistência de ferramentas voltadas para o ensino-aprendizagem de cálculo proposicional que atendessem aos critérios estabelecidos para um ambiente de suporte ao aluno (ASA). Como consequência do resultado da pesquisa, este trabalho introduz o conceito e os requisitos básicos de um ASA, concebe e implementa uma ferramenta ASA voltada para o ensino-aprendizagem de cálculo proposicional, acompanhada de um plano de ensino opcional, e os coloca à disposição da comunidade acadêmica. Apresenta também estudos de casos sobre apresentações e usos da ferramenta em vários estágios de desenvolvimento, além da descrição de cada módulo e dos métodos e regras disponibilizados pela ferramenta. Pretende-se que a ferramenta ASA-CalcPro e o plano de ensino sugerido, sejam uma contribuição social positiva e um estímulo ao ensino-aprendizagem de cálculo proposicional. / The adequate use of computational environments can increase the quality and comfort of the teaching-learning process for some of the academic disciplines. A review of the literature reveals the lack of existing tools for the teaching-learning of the propositional calculus that conform to the criteria established for the student support environment (ambiente de suporte ao aluno (ASA)). As a consequence of this conclusion, the current thesis introduces the concept of, and the basic requirements for, an ASA, conceives and implements an ASA tool for the teaching-learning of the propositional calculus, together with an optional teaching plan, and puts both at the disposition of the academic community. The thesis also presents case studies of presentations and uses of the tool at various stages of its development, as well as a description of each module and of the methods and rules made available for use by the tool. It is hoped that the ASA-CalcPro tool and the suggested plan of study will make a positive social contribution and will be a stimulant for the teaching-learning of the propositional calculus.

O ponto central dessa dissertação é expor categorialmente as funções de verdade do cálculo proposicional clássico, assim como provar, também categorialmente, que a definição dada se comporta tal como as tabelas de verdade dos operadores. Para tanto é feita uma exposição axiomática de teoria de categorias, salientando as construções e conceitos que servirão para o propósito principal da dissertação. É dada uma maior atenção ao conceito de Topos, estrutura onde as funções de verdade são em princípio construídas. Tal exposição é precedida de uma breve exposição da história de teoria de categorias. Por fim é apresentada uma possível nova estrutra, mais simples que Topos, onde também se constrói as funções de verdade. / The main purpose of this dissertation is to give a categorial account of the truth functions from the classic propositional calculus, as well as to prove, also categorially, that the definition given behave as the truth tables of the operators. For this end, an axiomatic exposition of category theory is made, focusing on constructions and concepts which will be used for the main purpose of the dissertation. More attention is given to the concept of Topos, structure where the truth functions are primarily constructed. Preceded by a brief exposition of Category Theory history. At the end, a new possible structure in which truth functions may be constructed, simpler than a Topos, is presented.

Thesis (Ph. D.)--University of Washington, 2004. / Vita. Includes bibliographical references (p. 106-117).

Thesis (Doctoral)--Technische Universiteit Eindhoven, 1996. / Contains summaries in English and Dutch. Vita. Includes bibliographical references (p. 145-154).

Η παρούσα διπλωµατική εργασία ασχολείται με το θέμα των Αλγορίθμων Επίλυσης Προβληµάτων SAT. Η εργασία αυτή εκπονήθηκε στα πλαίσια του Εργαστηρίου Ενσύρµατης Επικοινωνίας του Τµήματος Ηλεκτρολόγων Μηχανικών και Τεχνολογίας Υπολογιστών της Πολυτεχνικής Σχολής του Πανεπιστηµίου Πατρών. Σκοπός της είναι η δημιουργία ενός Προσομοιωτή των αλγορίθμων αυτών, ο οποίος να μπορεί να προσπελαστεί από οποιονδήποτε μέσω του διαδικτύου. Αρχικά έγινε µία εισαγωγή στο αντικείμενο της Τεχνητής Νοημοσύνης και πιο συγκεκριµένα στην Προτασιακή Λογική, ενώ δόθηκε και το απαραίτητο υπόβαθρο για να κατανοηθεί το πρόβληµμα και οι τεχνικές λύσης του. Τέλος, επιλέχθηκε να γίνει η υλοποίηση του Προσωμοιωτή σε Java. / This diploma dissertation deals with SAT solvers, algorithms for the Boolean satisfiability problem. It was produced in the Wire Communications Laboratory of the Electrical and Computer Engineering Department of the University of Patras. Its aim is to create a simulator for these algorithms, accessible to anyone via the Internet. An introduction to the field of Artificial Intelligence and more specifically to Propositional Calculus was given as well as the necessary groundwork to understand the problem and its solution approaches. The simulation implementation was developed in Java

Le thème central de la présente thèse est le contenu sémantique des quantificateurs logiques. Dans leur forme la plus simple, les quantificateurs permettent d’établir l’existence, ou la non-existence, d’individus répondant à une propriété. En tant que tels, ils incarnent la richesse et la complexité de la logique du premier ordre, par delà la logique propositionnelle. Nous contribuons à l’analyse sémantique des quantificateurs, du point de vue de la théorie de la dualité, dans trois domaines différents des mathématiques et de l’informatique théorique. D’une part, dans la théorie des langages formels à travers la logique sur les mots. D’autre part, dans la logique intuitionniste propositionnelle et dans l’étude de l’interpolation uniforme. Enfin, dans la topologie catégorique et dans la sémantique catégorique de la logique du premier ordre. / The unifying theme of the thesis is the semantic meaning of logical quantifiers. In their basic form quantifiers allow to state theexistence, or non-existence, of individuals satisfying a property. As such, they encode the richness and the complexity of predicate logic, as opposed to propositional logic. We contribute to the semantic understanding of quantifiers, from the viewpoint of duality theory, in three different areas of mathematics and theoretical computer science. First, in formal language theory through the syntactic approach provided by logic on words. Second, in intuitionistic propositional logic and in the study of uniform interpolation. Third, in categorical topology and categorical semantics for predicate logic.